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. inv (f x)) -> inv 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. inv (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. inv x) diffl -(inv x pow 2)) x

DIFF_INV

|- ∀f l x.
     (f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. inv (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 inv 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 inv 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 inv l) (f x)