Theory nets

⊢ ∀z. at z = atpointof mr1 z

⊢ at_infinity = mk_net (λx y. abs x ≥ abs y)

⊢ at_neginfinity = mk_net (λx y. x ≤ y)

⊢ at_posinfinity = mk_net (λx y. x ≥ y)

⊢ ∀m a. atpointof m a = mk_net (tendsto (m,a))

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

⊢ ∀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

⊢ ∀p net.
    eventually p net ⇔
    trivial_limit net ∨ ∃y. (∃x. netord net x y) ∧ ∀x. netord net x y ⇒ p x

⊢ ∀a v. (a in_direction v) = (at a within {b | ∃c. 0 ≤ c ∧ b − a = c * v})

⊢ ∀g. isnet g ⇔ ∀x y. (∀z. g z x ⇒ g z y) ∨ ∀z. g z y ⇒ g z x

⊢ ∀top f l net.
    limit top f l net ⇔
    l ∈ topspace top ∧
    ∀u. open_in top u ∧ l ∈ u ⇒ eventually (λx. f x ∈ u) net

⊢ ∃rep. TYPE_DEFINITION isnet rep

⊢ ∀net s.
    net_condition net s ⇔
    ∀x. x ∉ netlimits net ⇒ ∃y. y ∈ s ∧ netord net y x

⊢ ∀net. netfilter net = {{y | netord net y x} | x | x ∉ netlimits net}

⊢ ∀net. netlimit net = @a. ∀x. ¬netord net x a

⊢ ∀net. netlimits net = {a | ∀x. ¬netord net x a}

⊢ sequentially = mk_net (λm n. m ≥ n)

⊢ ∀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)

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

⊢ ∀net.
    trivial_limit net ⇔
    (∀a b. a = b) ∨ ∃a b. a ≠ b ∧ ∀x. ¬netord net x a ∧ ¬netord net x b

⊢ ∀net s. (net within s) = mk_net (λx y. netord net x y ∧ x ∈ s)

⊢ ∀net p. (∀x. p x) ⇒ eventually p net

⊢ ∀a x y. netord (at a) x y ⇔ 0 < dist (x,a) ∧ dist (x,a) ≤ dist (y,a)

⊢ ∀m a x y.
    netord (atpointof m a) x y ⇔
    0 < dist m (x,a) ∧ dist m (x,a) ≤ dist m (y,a)

⊢ ∀m a. (atpointof m a within mspace m) = atpointof m a

⊢ ∀x y. netord at_infinity x y ⇔ abs x ≥ abs y

⊢ ∀x y. netord at_neginfinity x y ⇔ x ≤ y

⊢ ∀x y. netord at_posinfinity x y ⇔ x ≥ y

⊢ ∀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

⊢ ∀net. dorder (netord net)

⊢ dorder $>=

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

⊢ ∀net. ∅ ∉ netfilter net

⊢ ∀net p q.
    eventually (λx. p x ∧ q x) net ⇔ eventually p net ∧ eventually q net

⊢ ∀p. eventually p at_infinity ⇔ ∃b. ∀x. abs x ≥ b ⇒ p x

⊢ ∀p. eventually p at_infinity ⇔ ∃b. 0 < b ∧ ∀x. abs x ≥ b ⇒ p x

⊢ ∀p. eventually p at_neginfinity ⇔ ∃b. ∀x. x ≤ b ⇒ p x

⊢ ∀p. eventually p at_posinfinity ⇔ ∃b. ∀x. x ≥ b ⇒ p x

⊢ ∀net. eventually (λx. F) net ⇔ trivial_limit net

⊢ ∀net p s.
    FINITE s ∧ s ≠ ∅ ⇒
    (eventually (λx. ∀a. a ∈ s ⇒ p a x) net ⇔
     ∀a. a ∈ s ⇒ eventually (p a) net)

⊢ ∀net p. eventually p net ⇒ trivial_limit net ∨ ∃x. p x

⊢ ∀net p q. (∀x. p x ⇒ q x) ∧ eventually p net ⇒ eventually q net

⊢ ∀net p q.
    eventually (λx. p x ⇒ q x) net ∧ eventually p net ⇒ eventually q net

⊢ ∀p. eventually p sequentially ⇔ ∃N. ∀n. N ≤ n ⇒ p n

⊢ ∀net. eventually (λx. T) net ⇔ T

⊢ ∀net p s.
    FINITE s ∧ s ≠ ∅ ⇒
    ((∀a. a ∈ s ⇒ eventually (p a) net) ⇔
     eventually (λx. ∀a. a ∈ s ⇒ p a x) net)

⊢ ∀a v x y.
    netord (a in_direction v) x y ⇔
    0 < dist (x,a) ∧ dist (x,a) ≤ dist (y,a) ∧ ∃c. 0 ≤ c ∧ x − a = c * v

⊢ ∀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)

⊢ ∀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)

⊢ (∀x. P x ⇒ Q x) ⇒ (∀x. P x) ⇒ ∀x. Q x

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

⊢ ∀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

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

⊢ ∀n x y.
    (∀z. netord n z x ⇒ netord n z y) ∨ ∀z. netord n z y ⇒ netord n z x

⊢ ∀n s t. s ∈ netfilter n ∧ t ∈ netfilter n ⇒ s ∩ t ∈ netfilter n

⊢ ∀a. netfilter (at a) =
      {{y | 0 < dist (y,a) ∧ dist (y,a) ≤ dist (x,a)} | x | x ≠ a}

⊢ ∀m a.
    netfilter (atpointof m a) =
    {{y | 0 < dist m (y,a) ∧ dist m (y,a) ≤ dist m (x,a)} | x | x ≠ a}

⊢ netfilter at_infinity = {{x | b ≤ abs x} | b ∈ 𝕌(:real)}

⊢ netfilter at_neginfinity = {{x | x ≤ a} | a ∈ 𝕌(:real)}

⊢ netfilter at_posinfinity = {{x | a ≤ x} | a ∈ 𝕌(:real)}

⊢ netfilter sequentially = {from n | n ∈ 𝕌(:num)}

⊢ ∀net s.
    net_condition net s ⇒
    netfilter (net within s) = netfilter net relative_to s

⊢ ∀a. netlimits (at a) = {a}

⊢ ∀m a. netlimits (atpointof m a) = {a}

⊢ ∀m a s.
    limpt (mtop m) a s ⇒
    netlimits (atpointof m a within s) = netlimits (atpointof m a)

⊢ netlimits at_infinity = ∅

⊢ netlimits at_neginfinity = ∅

⊢ netlimits at_posinfinity = ∅

⊢ ∀a s.
    net_condition (at a) s ⇒ netlimits (at a within s) = netlimits (at a)

⊢ netlimits sequentially = ∅

⊢ ∀net s. net_condition net s ⇒ netlimits (net within s) = netlimits net

⊢ ∀a. netlimit (at a) = a

⊢ ∀m a. netlimit (atpointof m a) = a

⊢ ∀a s. ¬trivial_limit (at a within s) ⇒ netlimit (at a within s) = a

⊢ ∀a s. net_condition (at a) s ⇒ netlimit (at a within s) = a

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

⊢ ∀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)

⊢ ∀a s. net_condition (at a) s ⇔ limpt (mtop mr1) a s

⊢ ∀m a s. limpt (mtop m) a s ⇒ net_condition (atpointof m a) s

⊢ ∀net s t. net_condition net s ∧ s ⊆ t ⇒ net_condition net t

⊢ ∀net s t.
    net_condition net s ∧ net_condition net s ⇒ net_condition net (s ∪ t)

⊢ net_condition net 𝕌(:α)

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

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

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

⊢ ∀net.
    (∃a. (∃x. netord net x a) ∧ ∀x. netord net x a ⇒ P x) ∧
    (∃b. (∃x. netord net x b) ∧ ∀x. netord net x b ⇒ Q x) ⇒
    ∃c. (∃x. netord net x c) ∧ ∀x. netord net x c ⇒ P x ∧ Q x

⊢ ∀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)

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

⊢ ∀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

⊢ ∀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)

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

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

⊢ ∀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)

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

⊢ ∀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)

⊢ ∀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. (net within 𝕌(:α)) = net

⊢ ∀net s. trivial_limit net ⇒ trivial_limit (net within s)

⊢ ∀net p. (∀x. ¬p x) ∧ ¬trivial_limit net ⇒ ¬eventually p net

⊢ ∀n x y.
    netord n x x ∧ netord n y y ⇒
    ∃z. netord n z z ∧ ∀w. netord n w z ⇒ netord n w x ∧ netord n w y

⊢ (∀e. 0 < e / 2 ⇔ 0 < e) ∧ (∀e. e / 2 + e / 2 = e) ∧ ∀e. 2 * (e / 2) = e

⊢ ∀m n. netord sequentially m n ⇔ m ≥ n

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

⊢ ¬trivial_limit at_infinity

⊢ ¬trivial_limit at_neginfinity

⊢ ¬trivial_limit at_posinfinity

⊢ ¬trivial_limit sequentially

⊢ ∀n s x y. netord (n within s) x y ⇔ netord n x y ∧ x ∈ s

⊢ ∀x. (at x within 𝕌(:real)) = at x

⊢ ∀net s t. ((net within s) within t) = (net within s ∩ t)

⊢ ∀a. at a = mk_net (λx y. 0 < dist (x,a) ∧ dist (x,a) ≤ dist (y,a))

⊢ ∀z. at z = mk_net (tendsto (mr1,z))

⊢ ∀m a.
    atpointof m a =
    mk_net (λx y. 0 < dist m (x,a) ∧ dist m (x,a) ≤ dist m (y,a))

⊢ ∀top f l net.
    ¬trivial_limit net ∧ l ∈ topspace top ∧
    (∀x y. netord net x y ⇒ netord net y y) ⇒
    (limit top f l net ⇔ (f tends l) (top,netord net))

⊢ (∀a. mk_net (netord a) = a) ∧
  ∀r. (∀x y. (∀z. r z x ⇒ r z y) ∨ ∀z. r z y ⇒ r z x) ⇔
      netord (mk_net r) = r

⊢ ∀n. netlimit n = @x. x ∈ netlimits n

⊢ ∀top f l net.
    ¬trivial_limit net ∧ l ∈ topspace top ⇒
    (f tends l) (top,netord net) ⇒
    limit top f l net

⊢ ∀m a. tendsto (m,a) = netord (atpointof m a)

⊢ ∀a. tendsto (mr1,a) = netord (at a)