Theory derivative

⊢ ∀f s. f concave_on s ⇔ (λx. -f x) convex_on s

⊢ ∀s. convex s ⇔
      ∀x y u v.
        x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒ u * x + v * y ∈ s

⊢ ∀f s.
    f convex_on s ⇔
    ∀x y u v.
      x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒
      f (u * x + v * y) ≤ u * f x + v * f y

⊢ ∀f net. f differentiable net ⇔ ∃f'. (f has_derivative f') net

⊢ ∀f s.
    f differentiable_on s ⇔ ∀x. x ∈ s ⇒ f differentiable (at x within s)

⊢ ∀x. exp x = suminf 𝕌(:num) (λn. (λn. (&FACT n)⁻¹) n * x pow n)

⊢ ∀f net. frechet_derivative f net = @f'. (f has_derivative f') net

⊢ ∀f f' net.
    (f has_derivative f') net ⇔
    linear f' ∧
    ((λy.
          (abs (y − netlimit net))⁻¹ *
          (f y − (f (netlimit net) + f' (y − netlimit net)))) ⟶ 0) net

⊢ ∀f f' net.
    (f has_vector_derivative f') net ⇔ (f has_derivative (λx. x * f')) net

⊢ ∀f. oabs f = sup {abs (f x) | abs x = 1}

⊢ ∀f net. vector_derivative f net = @f'. (f has_vector_derivative f') net

⊢ ∀f b.
    linear f ⇒
    ((∀x. abs x = 1 ⇒ abs (f x) ≤ b) ⇔ ∀x. abs (f x) ≤ b * abs x)

⊢ ∀f f' s.
    convex s ∧ (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ⇒
    (f concave_on s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ f y − f x ≤ f' x (y − x))

⊢ ∀f s.
    f concave_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment (a,b) ⇒
      (f b − f a) / abs (b − a) ≤ (f x − f a) / abs (x − a)

⊢ ∀f s.
    f concave_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment (a,b) ⇒
      (f b − f x) / abs (b − x) ≤ (f x − f a) / abs (x − a)

⊢ ∀f s.
    f concave_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment (a,b) ⇒
      (f b − f x) / abs (b − x) ≤ (f b − f a) / abs (b − a)

⊢ ∀f f' s.
    convex s ∧ (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ⇒
    (f concave_on s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ f' y (y − x) ≤ f y − f x)

⊢ ∀s. connected s ∧ compact s ⇔ ∃a b. s = interval [(a,b)]

⊢ ∀z. exp continuous at z

⊢ ∀s. exp continuous_on s

⊢ ∀s z. exp continuous (at z within s)

⊢ ∀s f g. f convex_on s ∧ g convex_on s ⇒ (λx. f x + g x) convex_on s

⊢ ∀a f s. (λx. a + f x) convex_on s ⇔ f convex_on s

⊢ ∀s. convex s ⇔
      ∀x y u. x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ u ≤ 1 ⇒ (1 − u) * x + u * y ∈ s

⊢ ∀x e. convex (ball (x,e))

⊢ ∀x e. convex (cball (x,e))

⊢ ∀s c f. 0 ≤ c ∧ f convex_on s ⇒ (λx. c * f x) convex_on s

⊢ ∀s. convex s ⇒ connected s

⊢ ∀s a b x. convex s ∧ a ∈ s ∧ b ∈ s ∧ x ∈ segment [(a,b)] ⇒ x ∈ s

⊢ ∀s. convex s ⇔ ∀a b. a ∈ s ∧ b ∈ s ⇒ segment (a,b) ⊆ s

⊢ ∀s. convex s ⇔ ∀a b. a ∈ s ∧ b ∈ s ⇒ segment [(a,b)] ⊆ s

⊢ ∀s. convex s ⇔ ∀a b. segment [(a,b)] ⊆ s ⇔ a ∈ s ∧ b ∈ s

⊢ ∀s a b. convex s ⇒ (segment [(a,b)] ⊆ s ⇔ a ∈ s ∧ b ∈ s)

⊢ ∀s a. (λx. dist (a,x)) convex_on s

⊢ convex ∅

⊢ ∀s. convex s ⇔
      ∀k u x.
        (∀i. 1 ≤ i ∧ i ≤ k ⇒ 0 ≤ u i ∧ x i ∈ s) ∧ sum {1 .. k} u = 1 ⇒
        sum {1 .. k} (λi. u i * x i) ∈ s

⊢ ∀s t. convex s ∧ convex t ⇒ convex (s ∩ t)

⊢ ∀f. (∀s. s ∈ f ⇒ convex s) ⇒ convex (BIGINTER f)

⊢ ∀a b. convex (interval [(a,b)]) ∧ convex (interval (a,b))

⊢ ∀f g s. f convex_on s ∧ g convex_on s ⇒ (λx. max (f x) (g x)) convex_on s

⊢ ∀s a. (λx. a) convex_on s

⊢ ∀f f' s.
    convex s ∧ (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ⇒
    (f convex_on s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ f' x (y − x) ≤ f' y (y − x))

⊢ ∀f f'x f'y s x y.
    f convex_on s ∧ segment [(x,y)] ⊆ s ∧
    (f has_derivative f'x) (at x within s) ∧
    (f has_derivative f'y) (at y within s) ⇒
    f'x (y − x) ≤ f'y (y − x)

⊢ ∀f f' s.
    convex s ∧ (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ⇒
    (f convex_on s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ f' x (y − x) ≤ f y − f x)

⊢ ∀f f' s x y.
    f convex_on s ∧ segment [(x,y)] ⊆ s ∧
    (f has_derivative f') (at x within s) ⇒
    f' (y − x) ≤ f y − f x

⊢ ∀f. f convex_on ∅

⊢ ∀f g s.
    convex s ∧ (∀x. x ∈ s ⇒ f x = g x) ∧ f convex_on s ⇒ g convex_on s

⊢ ∀f s.
    f convex_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment (a,b) ⇒
      (f x − f a) / abs (x − a) ≤ (f b − f a) / abs (b − a)

⊢ ∀f s.
    f convex_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment [(a,b)] ⇒
      (f x − f a) * abs (b − a) ≤ (f b − f a) * abs (x − a)

⊢ ∀f s.
    f convex_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment (a,b) ⇒
      (f x − f a) / abs (x − a) ≤ (f b − f x) / abs (b − x)

⊢ ∀f s.
    f convex_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment [(a,b)] ⇒
      (f x − f a) * abs (b − x) ≤ (f b − f x) * abs (x − a)

⊢ ∀f s.
    f convex_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment (a,b) ⇒
      (f b − f a) / abs (b − a) ≤ (f b − f x) / abs (b − x)

⊢ ∀f s.
    f convex_on s ⇔
    ∀a b x.
      a ∈ s ∧ b ∈ s ∧ x ∈ segment [(a,b)] ⇒
      (f b − f a) * abs (b − x) ≤ (f b − f x) * abs (b − a)

⊢ ∀f f' s.
    convex s ∧ (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ⇒
    (f convex_on s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ f y − f x ≤ f' y (y − x))

⊢ ∀f f' s x y.
    f convex_on s ∧ segment [(x,y)] ⊆ s ∧
    (f has_derivative f') (at y within s) ⇒
    f y − f x ≤ f' (y − x)

⊢ ∀f a. f convex_on {a}

⊢ ∀f s t. f convex_on t ∧ s ⊆ t ⇒ f convex_on s

⊢ ∀a. convex {a}

⊢ ∀s k u x.
    FINITE k ∧ convex s ∧ sum k u = 1 ∧ (∀i. i ∈ k ⇒ 0 ≤ u i ∧ x i ∈ s) ⇒
    sum k (λi. u i * x i) ∈ s

⊢ convex 𝕌(:real)

⊢ ∀f s. (∀x. x ∈ s ⇒ f differentiable at x) ⇒ f differentiable_on s

⊢ ∀f s x. f differentiable at x ⇒ f differentiable (at x within s)

⊢ ∀f f' s B.
    convex s ∧ (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ∧
    (∀x. x ∈ s ⇒ oabs (f' x) ≤ B) ⇒
    ∀x y. x ∈ s ∧ y ∈ s ⇒ abs (f x − f y) ≤ B * abs (x − y)

⊢ ∀f x. f differentiable at x ⇒ f continuous at x

⊢ ∀f s. f differentiable_on s ⇒ f continuous_on s

⊢ ∀f x s. f differentiable (at x within s) ⇒ f continuous (at x within s)

⊢ ∀f. f differentiable_on ∅

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x = g x) ∧ f differentiable_on s ⇒ g differentiable_on s

⊢ ∀f s.
    open s ⇒ (f differentiable_on s ⇔ ∀x. x ∈ s ⇒ f differentiable at x)

⊢ ∀f s t. f differentiable_on t ∧ s ⊆ t ⇒ f differentiable_on s

⊢ ∀f g x d.
    0 < d ∧ (∀x'. dist (x',x) < d ⇒ f x' = g x') ∧ f differentiable at x ⇒
    g differentiable at x

⊢ ∀f g x s d.
    0 < d ∧ x ∈ s ∧ (∀x'. x' ∈ s ∧ dist (x',x) < d ⇒ f x' = g x') ∧
    f differentiable (at x within s) ⇒
    g differentiable (at x within s)

⊢ ∀f a s.
    a ∈ s ∧ open s ⇒
    (f differentiable (at a within s) ⇔ f differentiable at a)

⊢ ∀f s t x.
    f differentiable (at x within t) ∧ s ⊆ t ⇒
    f differentiable (at x within s)

⊢ ∀f f' x s e.
    x ∈ s ∧ convex s ∧ (f has_derivative f') (at x within s) ∧ 0 < e ∧
    (∀w. w ∈ s ∩ ball (x,e) ⇒ f w ≤ f x) ⇒
    ∀y. y ∈ s ⇒ f' (y − x) ≤ 0

⊢ ∀f f' x s e.
    x ∈ s ∧ convex s ∧ (f has_derivative f') (at x within s) ∧ 0 < e ∧
    (∀w. w ∈ s ∩ ball (x,e) ⇒ f x ≤ f w) ⇒
    ∀y. y ∈ s ⇒ 0 ≤ f' (y − x)

⊢ ∀f f' x s.
    x ∈ s ∧ open s ∧ (f has_derivative f') (at x) ∧
    ((∀w. w ∈ s ⇒ f w ≤ f x) ∨ ∀w. w ∈ s ⇒ f x ≤ f w) ⇒
    ∀h. f' h = 0

⊢ ∀f f' x s.
    x ∈ s ∧ open s ∧ (f has_derivative f') (at x) ∧
    ((∀y. y ∈ s ⇒ f y ≤ f x) ∨ ∀y. y ∈ s ⇒ f x ≤ f y) ⇒
    f' = (λv. 0)

⊢ ∀f g f' g' x s.
    (f has_derivative f') (at x within s) ∧
    (g has_derivative g') (at (f x) within IMAGE f s) ⇒
    (g ∘ f has_derivative g' ∘ f') (at x within s)

⊢ ∀z. ((λn. z pow n / &FACT n) sums exp z) (from 0)

⊢ ∀R e.
    0 < R ∧ 0 < e ⇒
    ∃N. ∀n z.
      n ≥ N ∧ abs z < R ⇒
      abs (sum {0 .. n} (λi. z pow i / &FACT i) − exp z) ≤ e

⊢ ∀R e.
    0 < e ∧ 0 < R ⇒
    ∃N. ∀m n z.
      m ≥ N ∧ abs z ≤ R ⇒ abs (sum {m .. n} (λi. z pow i / &FACT i)) < e

⊢ ∀w z. ((λn. z pow n / &FACT n) sums w) (from 0) ⇔ w = exp z

⊢ ∀f net.
    f differentiable net ⇔ (f has_derivative frechet_derivative f net) net

⊢ ∀f f' g g' net.
    (f has_derivative f') net ∧ (g has_derivative g') net ⇒
    ((λx. f x + g x) has_derivative (λh. f' h + g' h)) net

⊢ ∀f f' x.
    (f has_derivative f') (at x) ⇔
    linear f' ∧
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀x'.
              0 < abs (x' − x) ∧ abs (x' − x) < d ⇒
              abs (f x' − f x − f' (x' − x)) / abs (x' − x) < e

⊢ ∀f f' x.
    (f has_derivative f') (at x) ⇔
    linear f' ∧
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀y. abs (y − x) < d ⇒
                abs (f y − f x − f' (y − x)) ≤ e * abs (y − x)

⊢ ∀f f' x s.
    (f has_derivative f') (at x) ⇒ (f has_derivative f') (at x within s)

⊢ ∀h f g f' g' x.
    (f has_derivative f') (at x) ∧ (g has_derivative g') (at x) ∧
    bilinear h ⇒
    ((λx. h (f x) (g x)) has_derivative
     (λd. h (f x) (g' d) + h (f' d) (g x))) (at x)

⊢ ∀h f g f' g' x s.
    (f has_derivative f') (at x within s) ∧
    (g has_derivative g') (at x within s) ∧ bilinear h ⇒
    ((λx. h (f x) (g x)) has_derivative
     (λd. h (f x) (g' d) + h (f' d) (g x))) (at x within s)

⊢ ∀f f' net c.
    (f has_derivative f') net ⇒
    ((λx. c * f x) has_derivative (λh. c * f' h)) net

⊢ ∀c net. ((λx. c) has_derivative (λh. 0)) net

⊢ ∀z. (exp has_derivative (λy. exp z * y)) (at z)

⊢ ∀net. ((λx. x) has_derivative (λh. h)) net

⊢ ∀f f' x. (f has_derivative f') (at x) ⇒ f continuous at x

⊢ ∀f f' net. (f has_derivative f') net ⇒ f differentiable net

⊢ ∀f net. linear f ⇒ (f has_derivative f) net

⊢ ∀f f' g g' a.
    (f has_derivative f') (at a) ∧ (g has_derivative g') (at a) ⇒
    ((λx. f x * g x) has_derivative (λh. f a * g' h + f' h * g a)) (at a)

⊢ ∀f f' g g' a s.
    (f has_derivative f') (at a within s) ∧
    (g has_derivative g') (at a within s) ⇒
    ((λx. f x * g x) has_derivative (λh. f a * g' h + f' h * g a))
      (at a within s)

⊢ ∀f f' net.
    (f has_derivative f') net ⇒ ((λx. -f x) has_derivative (λh. -f' h)) net

⊢ ∀q0 n.
    ((λq. q pow n) has_derivative
     (λq. sum {1 .. n} (λi. q0 pow (n − i) * q * q0 pow (i − 1)))) (at q0)

⊢ ∀s f f' g'.
    convex s ∧
    (∀n x. x ∈ s ⇒ (f n has_derivative f' n x) (at x within s)) ∧
    (∀e. 0 < e ⇒
         ∃N. ∀n x h. n ≥ N ∧ x ∈ s ⇒ abs (f' n x h − g' x h) ≤ e * abs h) ∧
    (∃x l. x ∈ s ∧ ((λn. f n x) ⟶ l) sequentially) ⇒
    ∃g. ∀x.
      x ∈ s ⇒
      ((λn. f n x) ⟶ g x) sequentially ∧
      (g has_derivative g' x) (at x within s)

⊢ ∀s f f' g'.
    convex s ∧
    (∀n x. x ∈ s ⇒ (f n has_derivative f' n x) (at x within s)) ∧
    (∀e. 0 < e ⇒
         ∃N. ∀n x h. n ≥ N ∧ x ∈ s ⇒ abs (f' n x h − g' x h) ≤ e * abs h) ⇒
    ∀e. 0 < e ⇒
        ∃N. ∀m n x y.
          m ≥ N ∧ n ≥ N ∧ x ∈ s ∧ y ∈ s ⇒
          abs (f m x − f n x − (f m y − f n y)) ≤ e * abs (x − y)

⊢ ∀s f f' g' k.
    convex s ∧
    (∀n x. x ∈ s ⇒ (f n has_derivative f' n x) (at x within s)) ∧
    (∀e. 0 < e ⇒
         ∃N. ∀n x h.
           n ≥ N ∧ x ∈ s ⇒
           abs (sum (k ∩ {x | 0 ≤ x ∧ x ≤ n}) (λi. f' i x h) − g' x h) ≤
           e * abs h) ∧ (∃x l. x ∈ s ∧ ((λn. f n x) sums l) k) ⇒
    ∃g. ∀x.
      x ∈ s ⇒
      ((λn. f n x) sums g x) k ∧ (g has_derivative g' x) (at x within s)

⊢ ∀s f f' g' k.
    convex s ∧
    (∀n x. x ∈ s ⇒ (f n has_derivative (λy. f' n x * y)) (at x within s)) ∧
    (∀e. 0 < e ⇒
         ∃N. ∀n x.
           n ≥ N ∧ x ∈ s ⇒ abs (sum (k ∩ {0 .. n}) (λi. f' i x) − g' x) ≤ e) ∧
    (∃x l. x ∈ s ∧ ((λn. f n x) sums l) k) ⇒
    ∃g. ∀x.
      x ∈ s ⇒
      ((λn. f n x) sums g x) k ∧
      (g has_derivative (λy. g' x * y)) (at x within s)

⊢ ∀f f' g g' net.
    (f has_derivative f') net ∧ (g has_derivative g') net ⇒
    ((λx. f x − g x) has_derivative (λh. f' h − g' h)) net

⊢ ∀f f' net s.
    FINITE s ∧ (∀a. a ∈ s ⇒ (f a has_derivative f' a) net) ⇒
    ((λx. sum s (λa. f a x)) has_derivative (λh. sum s (λa. f' a h))) net

⊢ ∀f f' g x d.
    0 < d ∧ (∀x'. dist (x',x) < d ⇒ f x' = g x') ∧
    (f has_derivative f') (at x) ⇒
    (g has_derivative f') (at x)

⊢ ∀f f' g x s d.
    0 < d ∧ x ∈ s ∧ (∀x'. x' ∈ s ∧ dist (x',x) < d ⇒ f x' = g x') ∧
    (f has_derivative f') (at x within s) ⇒
    (g has_derivative f') (at x within s)

⊢ ∀f f' x s.
    (f has_derivative f') (at x within s) ⇔
    linear f' ∧
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀x'.
              x' ∈ s ∧ 0 < abs (x' − x) ∧ abs (x' − x) < d ⇒
              abs (f x' − f x − f' (x' − x)) / abs (x' − x) < e

⊢ ∀f f' s x.
    (f has_derivative f') (at x within s) ⇔
    linear f' ∧
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀y. y ∈ s ∧ abs (y − x) < d ⇒
                abs (f y − f x − f' (y − x)) ≤ e * abs (y − x)

⊢ ∀f f' g x s.
    x ∈ s ∧ (∀x'. x' ∈ s ⇒ f x' = g x') ⇒
    ((f has_derivative f') (at x within s) ⇔
     (g has_derivative f') (at x within s))

⊢ ∀f f' a s.
    a ∈ s ∧ open s ⇒
    ((f has_derivative f') (at a within s) ⇔ (f has_derivative f') (at a))

⊢ ∀f f' s t x.
    (f has_derivative f') (at x within s) ∧ t ⊆ s ⇒
    (f has_derivative f') (at x within t)

⊢ ∀f f' x s.
    (f has_vector_derivative f') (at x) ⇒
    (f has_vector_derivative f') (at x within s)

⊢ ∀h f g f' g' x.
    (f has_vector_derivative f') (at x) ∧
    (g has_vector_derivative g') (at x) ∧ bilinear h ⇒
    ((λx. h (f x) (g x)) has_vector_derivative h (f x) g' + h f' (g x))
      (at x)

⊢ ∀h f g f' g' x s.
    (f has_vector_derivative f') (at x within s) ∧
    (g has_vector_derivative g') (at x within s) ∧ bilinear h ⇒
    ((λx. h (f x) (g x)) has_vector_derivative h (f x) g' + h f' (g x))
      (at x within s)

⊢ ∀f f' x s.
    (f has_vector_derivative f') (at x within s) ⇔
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀x'.
              x' ∈ s ∧ 0 < abs (x' − x) ∧ abs (x' − x) < d ⇒
              abs (f x' − f x − (x' − x) * f') / abs (x' − x) < e

⊢ ∀f f' x s.
    (f has_vector_derivative f') (at s within x) ⇔
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀y. y ∈ x ∧ abs (y − s) < d ⇒
                abs (f y − f s − (y − s) * f') ≤ e * abs (y − s)

⊢ ∀f f' a s.
    a ∈ s ∧ open s ⇒
    ((f has_vector_derivative f') (at a within s) ⇔
     (f has_vector_derivative f') (at a))

⊢ ∀f f' s t x.
    (f has_vector_derivative f') (at x within s) ∧ t ⊆ s ⇒
    (f has_vector_derivative f') (at x within t)

⊢ ∀s a b u.
    convex s ∧ a ∈ s ∧ b ∈ s ∧ 0 ≤ u ∧ u ≤ 1 ⇒ (1 − u) * a + u * b ∈ s

⊢ ∀s. is_interval s ⇒ connected s

⊢ ∀s. is_interval s ⇔ connected s

⊢ ∀s. is_interval s ⇒ convex s

⊢ ∀s. is_interval s ⇔ convex s

⊢ ∀s x. convex s ∧ x ∈ s ⇒ (x limit_point_of s ⇔ s ≠ {x})

⊢ ∀f a s.
    (f ⟶ 0) (at a within s) ⇒ ((λx. abs (x − a) * f x) ⟶ 0) (at a within s)

⊢ ∀f net. f differentiable net ⇒ linear (frechet_derivative f net)

⊢ ∀f s. linear f ⇒ f convex_on s

⊢ ∀f f' a b.
    a < b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ (f has_derivative f' x) (at x)) ⇒
    ∃x. x ∈ interval (a,b) ∧ f b − f a = f' x (b − a)

⊢ ∀f f' a b.
    a < b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ (f has_vector_derivative f' x) (at x)) ⇒
    ∃x. x ∈ interval (a,b) ∧ f b − f a = f' x * (b − a)

⊢ ∀f f' a b.
    a < b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ (f has_derivative f' x) (at x)) ⇒
    ∃x. x ∈ interval (a,b) ∧ abs (f b − f a) ≤ abs (f' x (b − a))

⊢ ∀f f' a b.
    a < b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ (f has_vector_derivative f' x) (at x)) ⇒
    ∃x. x ∈ interval (a,b) ∧ abs (f b − f a) ≤ abs (f' x * (b − a))

⊢ ∀f f' a b.
    a < b ∧
    (∀x. x ∈ interval [(a,b)] ⇒
         (f has_derivative f' x) (at x within interval [(a,b)])) ⇒
    ∃x. x ∈ interval (a,b) ∧ f b − f a = f' x (b − a)

⊢ ∀f f' a b.
    a ≤ b ∧
    (∀x. x ∈ interval [(a,b)] ⇒
         (f has_derivative f' x) (at x within interval [(a,b)])) ⇒
    ∃x. x ∈ interval [(a,b)] ∧ f b − f a = f' x (b − a)

⊢ ∀f. linear f ⇒
      (∀x. abs (f x) ≤ oabs f * abs x) ∧
      ∀b. (∀x. abs (f x) ≤ b * abs x) ⇒ oabs f ≤ b

⊢ ∀x y a b u v.
    x < a ∧ y < b ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒
    u * x + v * y < u * a + v * b

⊢ ∀x y a u v. x < a ∧ y < a ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒ u * x + v * y < a

⊢ ∀a b. a ≠ 0 ∧ b ≠ 0 ⇒ a * b ≠ 0

⊢ ∀f f' a b.
    a < b ∧ f a = f b ∧ f continuous_on interval [(a,b)] ∧
    (∀x. x ∈ interval (a,b) ⇒ (f has_derivative f' x) (at x)) ⇒
    ∃x. x ∈ interval (a,b) ∧ f' x = (λv. 0)

⊢ ∀s a b. convex s ∧ a ∈ s ∧ b ∈ s ⇒ segment [(a,b)] ⊆ s

⊢ ∀s x. convex s ∧ x ∈ s ⇒ (trivial_limit (at x within s) ⇔ s = {x})

⊢ ∀f s.
    f concave_on s ⇔
    ∀x y u v.
      x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒
      u * f x + v * f y ≤ f (u * x + v * y)

⊢ ∀f net. f differentiable net ⇔ ∃l. (f has_vector_derivative l) net

⊢ ∀f f' x.
    (f has_derivative f') (at x) ⇔
    linear f' ∧
    ((λy. (abs (y − x))⁻¹ * (f y − (f x + f' (y − x)))) ⟶ 0) (at x)

⊢ ∀f net.
    (∃f'. (f has_derivative f') net) ⇔ ∃l. (f has_vector_derivative l) net

⊢ ∀f f' x s.
    (f has_derivative f') (at x within s) ⇔
    linear f' ∧
    ((λy. (abs (y − x))⁻¹ * (f y − (f x + f' (y − x)))) ⟶ 0)
      (at x within s)

⊢ ∀f l x s.
    (f has_vector_derivative l) (at x within s) ⇔
    ((λy. (abs (y − x))⁻¹ * (f y − (f x + l * (y − x)))) ⟶ 0)
      (at x within s)