Theory "lim"

Parents seq

Signature

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

Definitions

contl

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

differentiable

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

diffl

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

tends_real_real

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

Theorems

CONTL_LIM

⊢ ∀f x. f contl x ⇔ (f → f x) x

CONT_ADD

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x + g x) contl 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

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_COMPOSE

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

CONT_CONST

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

CONT_DIV

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

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_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_INV

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

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

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_SUB

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x − g x) contl 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_CARAT

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

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_CMUL

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

DIFF_CONST

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

DIFF_CONT

⊢ ∀f l x. (f diffl l) x ⇒ f contl 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)²)) x

DIFF_INV

⊢ ∀f l x. (f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. (f x)⁻¹) diffl -(l / (f x)²)) 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)

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)

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

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_LCONST

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

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_LINC

⊢ ∀f x l.
    (f diffl l) x ∧ 0 < l ⇒ ∃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_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_NEG

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

DIFF_POW

⊢ ∀n x. ((λx. x pow n) diffl (&n * x pow (n − 1))) 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_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

DIFF_UNIQ

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

DIFF_X

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

DIFF_XM1

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

INTERVAL_ABS

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

INTERVAL_CLEMMA

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

INTERVAL_LEMMA

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

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)

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_ADD

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

LIM_CONST

⊢ ∀k x. ((λx. k) → k) 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_EQUAL

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

LIM_INV

⊢ ∀f l x. (f → l) x ∧ l ≠ 0 ⇒ ((λx. (f x)⁻¹) → l⁻¹) 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_NULL

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

LIM_SUB

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

LIM_TRANSFORM

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

LIM_UNIQ

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

LIM_X

⊢ ∀x0. ((λx. x) → x0) x0

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)

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

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