Theory "lim"

Parents seq

Signature

Constant	Type
contl	:(real -> real) -> real -> bool
differentiable	:(real -> real) -> real -> bool
diffl	:(real -> real) -> real reln
tends_real_real	:(real -> real) -> real reln

Definitions

tends_real_real

⊢ ∀f l x0. (f -> l) x0 ⇔ (f tends l) (mtop mr1,tendsto (mr1,x0))

diffl

⊢ ∀f l x. (f diffl l) x ⇔ ((λh. (f (x + h) − f x) / h) -> l) 0

contl

⊢ ∀f x. f contl x ⇔ ((λh. f (x + h)) -> f x) 0

differentiable

⊢ ∀f x. f differentiable x ⇔ ∃l. (f diffl l) x

Theorems

LIM

⊢ ∀f y0 x0.
      (f -> y0) x0 ⇔
      ∀e.
          0 < e ⇒
          ∃d.
              0 < d ∧
              ∀x. 0 < abs (x − x0) ∧ abs (x − x0) < d ⇒ abs (f x − y0) < e

LIM_CONST

⊢ ∀k x. ((λx. k) -> k) x

LIM_ADD

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x + g x) -> l + m) x

LIM_MUL

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x * g x) -> l * m) x

LIM_NEG

⊢ ∀f l x. (f -> l) x ⇔ ((λx. -f x) -> -l) x

LIM_INV

⊢ ∀f l x. (f -> l) x ∧ l ≠ 0 ⇒ ((λx. (f x)⁻¹) -> l⁻¹) x

LIM_SUB

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x − g x) -> l − m) x

LIM_DIV

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ∧ m ≠ 0 ⇒ ((λx. f x / g x) -> l / m) x

LIM_NULL

⊢ ∀f l x. (f -> l) x ⇔ ((λx. f x − l) -> 0) x

LIM_X

⊢ ∀x0. ((λx. x) -> x0) x0

LIM_UNIQ

⊢ ∀f l m x. (f -> l) x ∧ (f -> m) x ⇒ l = m

LIM_EQUAL

⊢ ∀f g l x0. (∀x. x ≠ x0 ⇒ f x = g x) ⇒ ((f -> l) x0 ⇔ (g -> l) x0)

LIM_TRANSFORM

⊢ ∀f g x0 l. ((λx. f x − g x) -> 0) x0 ∧ (g -> l) x0 ⇒ (f -> l) x0

DIFF_UNIQ

⊢ ∀f l m x. (f diffl l) x ∧ (f diffl m) x ⇒ l = m

DIFF_CONT

⊢ ∀f l x. (f diffl l) x ⇒ f contl x

CONTL_LIM

⊢ ∀f x. f contl x ⇔ (f -> f x) x

DIFF_CARAT

⊢ ∀f l x.
      (f diffl l) x ⇔
      ∃g. (∀z. f z − f x = g z * (z − x)) ∧ g contl x ∧ g x = l

CONT_CONST

⊢ ∀k x. (λx. k) contl x

CONT_ADD

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

CONT_MUL

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x * g x) contl x

CONT_NEG

⊢ ∀f x. f contl x ⇒ (λx. -f x) contl x

CONT_INV

⊢ ∀f x. f contl x ∧ f x ≠ 0 ⇒ (λx. (f x)⁻¹) contl x

CONT_SUB

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x − g x) contl x

CONT_DIV

⊢ ∀f g x. f contl x ∧ g contl x ∧ g x ≠ 0 ⇒ (λx. f x / g x) contl x

CONT_COMPOSE

⊢ ∀f g x. f contl x ∧ g contl f x ⇒ (λx. g (f x)) contl x

IVT

⊢ ∀f a b y.
      a ≤ b ∧ (f a ≤ y ∧ y ≤ f b) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃x. a ≤ x ∧ x ≤ b ∧ f x = y

IVT2

⊢ ∀f a b y.
      a ≤ b ∧ (f b ≤ y ∧ y ≤ f a) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃x. a ≤ x ∧ x ≤ b ∧ f x = y

DIFF_CONST

⊢ ∀k x. ((λx. k) diffl 0) x

DIFF_ADD

⊢ ∀f g l m x.
      (f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x + g x) diffl (l + m)) x

DIFF_MUL

⊢ ∀f g l m x.
      (f diffl l) x ∧ (g diffl m) x ⇒
      ((λx. f x * g x) diffl (l * g x + m * f x)) x

DIFF_CMUL

⊢ ∀f c l x. (f diffl l) x ⇒ ((λx. c * f x) diffl (c * l)) x

DIFF_NEG

⊢ ∀f l x. (f diffl l) x ⇒ ((λx. -f x) diffl -l) x

DIFF_SUB

⊢ ∀f g l m x.
      (f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x − g x) diffl (l − m)) x

DIFF_CHAIN

⊢ ∀f g l m x.
      (f diffl l) (g x) ∧ (g diffl m) x ⇒ ((λx. f (g x)) diffl (l * m)) x

DIFF_X

⊢ ∀x. ((λx. x) diffl 1) x

DIFF_POW

⊢ ∀n x. ((λx. x pow n) diffl (&n * x pow (n − 1))) x

DIFF_XM1

⊢ ∀x. x ≠ 0 ⇒ ((λx. x⁻¹) diffl -(x⁻¹ pow 2)) x

DIFF_INV

⊢ ∀f l x. (f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. (f x)⁻¹) diffl -(l / f x pow 2)) x

DIFF_DIV

⊢ ∀f g l m x.
      (f diffl l) x ∧ (g diffl m) x ∧ g x ≠ 0 ⇒
      ((λx. f x / g x) diffl ((l * g x − m * f x) / g x pow 2)) x

DIFF_SUM

⊢ ∀f f' m n x.
      (∀r. m ≤ r ∧ r < m + n ⇒ ((λx. f r x) diffl f' r x) x) ⇒
      ((λx. sum (m,n) (λn. f n x)) diffl sum (m,n) (λr. f' r x)) x

CONT_BOUNDED

⊢ ∀f a b.
      a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃M. ∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M

CONT_HASSUP

⊢ ∀f a b.
      a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃M.
          (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧
          ∀N. N < M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ N < f x

CONT_ATTAINS

⊢ ∀f a b.
      a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ f x = M

CONT_ATTAINS2

⊢ ∀f a b.
      a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ M ≤ f x) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ f x = M

CONT_ATTAINS_ALL

⊢ ∀f a b.
      a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
      ∃L M.
          L ≤ M ∧ (∀y. L ≤ y ∧ y ≤ M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ f x = y) ∧
          ∀x. a ≤ x ∧ x ≤ b ⇒ L ≤ f x ∧ f x ≤ M

DIFF_LINC

⊢ ∀f x l.
      (f diffl l) x ∧ 0 < l ⇒ ∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x + h)

DIFF_LDEC

⊢ ∀f x l.
      (f diffl l) x ∧ l < 0 ⇒ ∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x − h)

DIFF_LMAX

⊢ ∀f x l.
      (f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f y ≤ f x) ⇒ l = 0

DIFF_LMIN

⊢ ∀f x l.
      (f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f x ≤ f y) ⇒ l = 0

DIFF_LCONST

⊢ ∀f x l.
      (f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f y = f x) ⇒ l = 0

INTERVAL_LEMMA

⊢ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ a ≤ y ∧ y ≤ b

ROLLE

⊢ ∀f a b.
      a < b ∧ f a = f b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
      (∀x. a < x ∧ x < b ⇒ f differentiable x) ⇒
      ∃z. a < z ∧ z < b ∧ (f diffl 0) z

MVT_LEMMA

⊢ ∀f a b.
      (λx. f x − (f b − f a) / (b − a) * x) a =
      (λx. f x − (f b − f a) / (b − a) * x) b

MVT

⊢ ∀f a b.
      a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
      (∀x. a < x ∧ x < b ⇒ f differentiable x) ⇒
      ∃l z. a < z ∧ z < b ∧ (f diffl l) z ∧ f b − f a = (b − a) * l

DIFF_ISCONST_END

⊢ ∀f a b.
      a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
      (∀x. a < x ∧ x < b ⇒ (f diffl 0) x) ⇒
      f b = f a

DIFF_ISCONST

⊢ ∀f a b.
      a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
      (∀x. a < x ∧ x < b ⇒ (f diffl 0) x) ⇒
      ∀x. a ≤ x ∧ x ≤ b ⇒ f x = f a

DIFF_ISCONST_ALL

⊢ ∀f. (∀x. (f diffl 0) x) ⇒ ∀x y. f x = f y

INTERVAL_ABS

⊢ ∀x z d. x − d ≤ z ∧ z ≤ x + d ⇔ abs (z − x) ≤ d

CONT_INJ_LEMMA

⊢ ∀f g x d.
      0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ g (f z) = z) ∧
      (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
      ¬∀z. abs (z − x) ≤ d ⇒ f z ≤ f x

CONT_INJ_LEMMA2

⊢ ∀f g x d.
      0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ g (f z) = z) ∧
      (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
      ¬∀z. abs (z − x) ≤ d ⇒ f x ≤ f z

CONT_INJ_RANGE

⊢ ∀f g x d.
      0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ g (f z) = z) ∧
      (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
      ∃e. 0 < e ∧ ∀y. abs (y − f x) ≤ e ⇒ ∃z. abs (z − x) ≤ d ∧ f z = y

CONT_INVERSE

⊢ ∀f g x d.
      0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ g (f z) = z) ∧
      (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
      g contl f x

DIFF_INVERSE

⊢ ∀f g l x d.
      0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ g (f z) = z) ∧
      (∀z. abs (z − x) ≤ d ⇒ f contl z) ∧ (f diffl l) x ∧ l ≠ 0 ⇒
      (g diffl l⁻¹) (f x)

DIFF_INVERSE_LT

⊢ ∀f g l x d.
      0 < d ∧ (∀z. abs (z − x) < d ⇒ g (f z) = z) ∧
      (∀z. abs (z − x) < d ⇒ f contl z) ∧ (f diffl l) x ∧ l ≠ 0 ⇒
      (g diffl l⁻¹) (f x)

INTERVAL_CLEMMA

⊢ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (y − x) ≤ d ⇒ a < y ∧ y < b

DIFF_INVERSE_OPEN

⊢ ∀f g l a x b.
      a < x ∧ x < b ∧ (∀z. a < z ∧ z < b ⇒ g (f z) = z ∧ f contl z) ∧
      (f diffl l) x ∧ l ≠ 0 ⇒
      (g diffl l⁻¹) (f x)