Theory: nets

Parents

• topology

Types

Constants

• dorder  :('a -> 'a -> bool) -> bool
• bounded  :'a metric # ('b -> 'b -> bool) -> ('b -> 'a) -> bool
• tends  :('b -> 'a) -> 'a -> 'a topology # ('b -> 'b -> bool) -> bool
• tendsto  :'a metric # 'a -> 'a -> 'a -> bool

Definitions

bounded

|- !m g f. bounded (m,g) f = ?k x N. g N N /\ !n. g n N ==> dist m (f n,x) < k

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

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)

tendsto

|- !m x y z.
     tendsto (m,x) y z = 0 < dist m (x,y) /\ dist m (x,y) <= dist m (x,z)

Theorems

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

DORDER_NGE

|- dorder $>=

DORDER_TENDSTO

|- !m x. dorder (tendsto (m,x))

LIM_TENDS

|- !m1 m2 f x0 y0.
     limpt (mtop m1) x0 re_universe ==>
     ((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_TENDS2

|- !m1 m2 f x0 y0.
     limpt (mtop m1) x0 re_universe ==>
     ((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)

MR1_BOUNDED

|- !g f. bounded (mr1,g) f = ?k N. g N N /\ !n. g n N ==> abs (f n) < k

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

MTOP_TENDS_UNIQ

|- !g d.
     dorder g ==>
     (x tends x0) (mtop d,g) /\ (x tends x1) (mtop d,g) ==>
     (x0 = x1)

NET_ABS

|- !g x x0.
     (x tends x0) (mtop mr1,g) ==> ((\n. abs (x n)) tends abs x0) (mtop mr1,g)

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_CONV_BOUNDED

|- !g x x0. (x tends x0) (mtop mr1,g) ==> bounded (mr1,g) x

NET_CONV_IBOUNDED

|- !g x x0.
     (x tends x0) (mtop mr1,g) /\ ~(x0 = 0) ==>
     bounded (mr1,g) (\n. inv (x n))

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

|- !g.
     dorder g ==>
     !x x0.
       (x tends x0) (mtop mr1,g) /\ ~(x0 = 0) ==>
       ((\n. inv (x n)) tends inv x0) (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_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_NEG

|- !g.
     dorder g ==>
     !x x0. (x tends x0) (mtop mr1,g) = ((\n. ~x n) tends ~x0) (mtop mr1,g)

NET_NULL

|- !g x x0. (x tends x0) (mtop mr1,g) = ((\n. x n - x0) 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_CMUL

|- !g k x. (x tends 0) (mtop mr1,g) ==> ((\n. k * x n) tends 0) (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_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)

SEQ_TENDS

|- !d x x0.
     (x tends x0) (mtop d,$>=) =
     !e. 0 < e ==> ?N. !n. n >= N ==> dist d (x n,x0) < e