Theory "nets"

Signature

Definitions

tendsto

⊢ ∀m x y z. tendsto (m,x) y z ⇔ 0 < dist m (x,y) ∧ dist m (x,y) ≤ dist m (x,z)

tends

⊢ ∀s l top g.
      (s tends l) (top,g) ⇔
      ∀N. neigh top (N,l) ⇒ ∃n. g n n ∧ ∀m. g m n ⇒ N (s m)

dorder

⊢ ∀g. dorder g ⇔ ∀x y. g x x ∧ g y y ⇒ ∃z. g z z ∧ ∀w. g w z ⇒ g w x ∧ g w y

bounded

⊢ ∀m g f. bounded (m,g) f ⇔ ∃k x N. g N N ∧ ∀n. g n N ⇒ dist m (f n,x) < k

Theorems

SEQ_TENDS

⊢ ∀d x x0.
      (x tends x0) (mtop d,$>=) ⇔
      ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ dist d (x n,x0) < e

NET_SUB

⊢ ∀g.
      dorder g ⇒
      ∀x x0 y y0.
          (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ⇒
          ((λn. x n − y n) tends (x0 − y0)) (mtop mr1,g)

NET_NULL_MUL

⊢ ∀g.
      dorder g ⇒
      ∀x y.
          bounded (mr1,g) x ∧ (y tends 0) (mtop mr1,g) ⇒
          ((λn. x n * y n) tends 0) (mtop mr1,g)

NET_NULL_CMUL

⊢ ∀g k x. (x tends 0) (mtop mr1,g) ⇒ ((λn. k * x n) tends 0) (mtop mr1,g)

NET_NULL_ADD

⊢ ∀g.
      dorder g ⇒
      ∀x y.
          (x tends 0) (mtop mr1,g) ∧ (y tends 0) (mtop mr1,g) ⇒
          ((λn. x n + y n) tends 0) (mtop mr1,g)

NET_NULL

⊢ ∀g x x0. (x tends x0) (mtop mr1,g) ⇔ ((λn. x n − x0) tends 0) (mtop mr1,g)

NET_NEG

⊢ ∀g.
      dorder g ⇒
      ∀x x0. (x tends x0) (mtop mr1,g) ⇔ ((λn. -x n) tends -x0) (mtop mr1,g)

NET_MUL

⊢ ∀g.
      dorder g ⇒
      ∀x y x0 y0.
          (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ⇒
          ((λn. x n * y n) tends (x0 * y0)) (mtop mr1,g)

NET_LE

⊢ ∀g.
      dorder g ⇒
      ∀x x0 y y0.
          (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ∧
          (∃N. g N N ∧ ∀n. g n N ⇒ x n ≤ y n) ⇒
          x0 ≤ y0

NET_INV

⊢ ∀g.
      dorder g ⇒
      ∀x x0.
          (x tends x0) (mtop mr1,g) ∧ x0 ≠ 0 ⇒
          ((λn. (x n)⁻¹) tends x0⁻¹) (mtop mr1,g)

NET_DIV

⊢ ∀g.
      dorder g ⇒
      ∀x x0 y y0.
          (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ∧ y0 ≠ 0 ⇒
          ((λn. x n / y n) tends (x0 / y0)) (mtop mr1,g)

NET_CONV_NZ

⊢ ∀g x x0.
      (x tends x0) (mtop mr1,g) ∧ x0 ≠ 0 ⇒ ∃N. g N N ∧ ∀n. g n N ⇒ x n ≠ 0

NET_CONV_IBOUNDED

⊢ ∀g x x0. (x tends x0) (mtop mr1,g) ∧ x0 ≠ 0 ⇒ bounded (mr1,g) (λn. (x n)⁻¹)

NET_CONV_BOUNDED

⊢ ∀g x x0. (x tends x0) (mtop mr1,g) ⇒ bounded (mr1,g) x

NET_ADD

⊢ ∀g.
      dorder g ⇒
      ∀x x0 y y0.
          (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ⇒
          ((λn. x n + y n) tends (x0 + y0)) (mtop mr1,g)

NET_ABS

⊢ ∀g x x0.
      (x tends x0) (mtop mr1,g) ⇒ ((λn. abs (x n)) tends abs x0) (mtop mr1,g)

MTOP_TENDS_UNIQ

⊢ ∀g d.
      dorder g ⇒ (x tends x0) (mtop d,g) ∧ (x tends x1) (mtop d,g) ⇒ (x0 = x1)

MTOP_TENDS

⊢ ∀d g x x0.
      (x tends x0) (mtop d,g) ⇔
      ∀e. 0 < e ⇒ ∃n. g n n ∧ ∀m. g m n ⇒ dist d (x m,x0) < e

MR1_BOUNDED

⊢ ∀g f. bounded (mr1,g) f ⇔ ∃k N. g N N ∧ ∀n. g n N ⇒ abs (f n) < k

LIM_TENDS2

⊢ ∀m1 m2 f x0 y0.
      limpt (mtop m1) x0 𝕌(:α) ⇒
      ((f tends y0) (mtop m2,tendsto (m1,x0)) ⇔
       ∀e.
           0 < e ⇒
           ∃d.
               0 < d ∧
               ∀x.
                   0 < dist m1 (x,x0) ∧ dist m1 (x,x0) < d ⇒
                   dist m2 (f x,y0) < e)

LIM_TENDS

⊢ ∀m1 m2 f x0 y0.
      limpt (mtop m1) x0 𝕌(:α) ⇒
      ((f tends y0) (mtop m2,tendsto (m1,x0)) ⇔
       ∀e.
           0 < e ⇒
           ∃d.
               0 < d ∧
               ∀x.
                   0 < dist m1 (x,x0) ∧ dist m1 (x,x0) ≤ d ⇒
                   dist m2 (f x,y0) < e)

DORDER_TENDSTO

⊢ ∀m x. dorder (tendsto (m,x))

DORDER_NGE

⊢ dorder $>=

DORDER_LEMMA

⊢ ∀g.
      dorder g ⇒
      ∀P Q.
          (∃n. g n n ∧ ∀m. g m n ⇒ P m) ∧ (∃n. g n n ∧ ∀m. g m n ⇒ Q m) ⇒
          ∃n. g n n ∧ ∀m. g m n ⇒ P m ∧ Q m