Theory metric

⊢ ∀E1 E2 k f.
    Lipschitz_condition (E1,E2) k f ⇔
    ∀x y. dist E2 (f x,f y) ≤ k * dist E1 (x,y)

⊢ ∀E1 E2 f.
    Lipschitz_continuous_map (E1,E2) f ⇔
    ∃k. 0 < k ∧ Lipschitz_condition (E1,E2) k f

⊢ ∀m x e. mball m (x,e) = (λy. dist m (x,y) < e)

⊢ ∀m. bounded_metric m = metric (λ(x,y). dist m (x,y) / (1 + dist m (x,y)))

⊢ dist = dist mr1

⊢ ∀top. fsigma_in top = countable UNION_OF closed_in top

⊢ ∀top.
    gdelta_in top =
    countable INTERSECTION_OF open_in top relative_to topspace top

⊢ ∀m. ismet m ⇔
      (∀x y. m (x,y) = 0 ⇔ x = y) ∧ ∀x y z. m (y,z) ≤ m (x,y) + m (x,z)

⊢ ∀m x r.
    mcball m (x,r) = {y | x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) ≤ r}

⊢ ∃rep. TYPE_DEFINITION ismet rep

⊢ (∀a. metric (dist a) = a) ∧ ∀r. ismet r ⇔ dist (metric r) = r

⊢ ∀top. metrizable_space top ⇔ ∃m. top = mtop m

⊢ mr1 = metric (λ(x,y). abs (y − x))

⊢ mr2 = metric (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))

⊢ ∀m. mspace m = topspace (mtop m)

⊢ ∀m. mtop m =
      topology (λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)

⊢ ∀d s t.
    set_dist d (s,t) =
    if s = ∅ ∨ t = ∅ then 0 else inf {dist d (x,y) | x ∈ s ∧ y ∈ t}

⊢ ∀m s e. set_mcball m s e = {x | set_dist m ({x},s) ≤ e}

⊢ ∀m x e. 0 < e ⇒ neigh (mtop m) (mball m (x,e),x)

⊢ ∀m x e. 0 < e ⇒ open_in (mtop m) (mball m (x,e))

⊢ ∀m x r. 0 < r ∧ x ∈ mspace m ⇒ x ∈ mball m (x,r)

⊢ ∀m x r. x ∈ mball m (x,r) ⇔ x ∈ mspace m ∧ 0 < r

⊢ ∀m x r. 0 ≤ r ∧ x ∈ mspace m ⇒ x ∈ mcball m (x,r)

⊢ ∀m x r. x ∈ mcball m (x,r) ⇔ x ∈ mspace m ∧ 0 ≤ r

⊢ ∀top s. closed_in top s ⇒ fsigma_in top s

⊢ ∀top s. metrizable_space top ∧ closed_in top s ⇒ gdelta_in top s

⊢ ∀m x r. closed_in (mtop m) (mcball m (x,r))

⊢ ∀m c.
    closed_in (mtop m) c ⇔
    c ⊆ mspace m ∧
    ∀x. x ∈ mspace m DIFF c ⇒ ∃r. 0 < r ∧ DISJOINT c (mball m (x,r))

⊢ ∀m top f.
    continuous_map (mtop m,top) f ⇔
    IMAGE f (mspace m) ⊆ topspace top ∧
    ∀a. a ∈ mspace m ⇒
        ∀u. open_in top u ∧ f a ∈ u ⇒
            ∃d. 0 < d ∧ ∀x. x ∈ mspace m ∧ dist m (a,x) < d ⇒ f x ∈ u

⊢ ∀t m f.
    continuous_map (t,mtop m) f ⇔
    ∀x. x ∈ topspace t ⇒
        ∀r. 0 < r ⇒
            ∃u. open_in t u ∧ x ∈ u ∧ ∀y. y ∈ u ⇒ f y ∈ mball m (f x,r)

⊢ ∀x. dist (x,0) = abs x ∧ dist (0,x) = abs x

⊢ ∀x y c. dist (x + c,y + c) = dist (x,y)

⊢ ∀w x y z. dist (w,x) = dist (y,z) ⇔ (dist (w,x))² = (dist (y,z))²

⊢ ∀x y. dist (x,y) = 0 ⇔ x = y

⊢ ∀x y. dist (x,y) ≤ 0 ⇔ x = y

⊢ ∀x y c. dist (c * x,c * y) = abs c * dist (x,y)

⊢ ∀x y. x ≠ y ⇔ 0 < dist (x,y)

⊢ ∀x y. 0 ≤ dist (x,y)

⊢ ∀x y. x ≠ y ⇒ 0 < dist (x,y)

⊢ ∀x. dist (x,x) = 0

⊢ ∀x y. dist (x,y) = dist (y,x)

⊢ ∀x y z. dist (x,z) ≤ dist (x,y) + dist (y,z)

⊢ ∀x x' y y'. dist (x + y,x' + y') ≤ dist (x,x') + dist (y,y')

⊢ ∀x x' y y'.
    dist (x,x') < e / 2 ∧ dist (y,y') < e / 2 ⇒ dist (x + y,x' + y') < e

⊢ ∀x y z. dist (y,z) ≤ dist (x,y) + dist (x,z)

⊢ ∀x1 x2 y. dist (x1,y) < e / 2 ∧ dist (x2,y) < e / 2 ⇒ dist (x1,x2) < e

⊢ ∀x1 x2 y. dist (y,x1) < e / 2 ∧ dist (y,x2) < e / 2 ⇒ dist (x1,x2) < e

⊢ ∀x y z e. dist (x,z) + dist (y,z) ≤ e ⇒ dist (x,y) ≤ e

⊢ ∀x y z e. dist (x,z) + dist (y,z) < e ⇒ dist (x,y) < e

⊢ ∀P. (∃top. metrizable_space top ∧ P top (topspace top)) ⇔
      ∃m. P (mtop m) (mspace m)

⊢ ∀P. (∀m. P (mtop m) (mspace m)) ⇔
      ∀top. metrizable_space top ⇒ P top (topspace top)

⊢ ∀P. (∀top. metrizable_space top ⇒ P top (topspace top)) ⇔
      ∀m. P (mtop m) (mspace m)

⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ∧ (∀n. n ≠ 0 ⇒ P (&n)⁻¹) ⇒ ∀e. 0 < e ⇒ P e

⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ∧ (∀n. P (&n + 1)⁻¹) ⇒ ∀e. 0 < e ⇒ P e

⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ⇒ ((∀e. 0 < e ⇒ P e) ⇔ ∀n. P (&n + 1)⁻¹)

⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ⇒
      ((∀e. 0 < e ⇒ P e) ⇔ ∀n. n ≠ 0 ⇒ P (&n)⁻¹)

⊢ (∀n. n ≠ 0 ⇒ P n) ⇔ ∀n. P (SUC n)

⊢ ∀top s.
    fsigma_in top s ⇔
    ∃c. (∀n. closed_in top (c n)) ∧ (∀n. c n ⊆ c (n + 1)) ∧
        BIGUNION {c n | n ∈ 𝕌(:num)} = s

⊢ ∀top s t. fsigma_in top s ∧ gdelta_in top t ⇒ fsigma_in top (s DIFF t)

⊢ ∀top. fsigma_in top ∅

⊢ ∀top s t.
    fsigma_in top s ⇒
    (fsigma_in (subtopology top s) t ⇔ fsigma_in top t ∧ t ⊆ s)

⊢ ∀top s.
    fsigma_in top s ⇔
    s ⊆ topspace top ∧ gdelta_in top (topspace top DIFF s)

⊢ ∀top s t. fsigma_in top s ∧ fsigma_in top t ⇒ fsigma_in top (s ∩ t)

⊢ ∀top s. fsigma_in top relative_to s = fsigma_in (subtopology top s)

⊢ ∀top. fsigma_in top relative_to topspace top = fsigma_in top

⊢ ∀top s. fsigma_in top s ⇒ s ⊆ topspace top

⊢ ∀top u s.
    fsigma_in (subtopology top u) s ⇔ ∃t. fsigma_in top t ∧ s = t ∩ u

⊢ ∀top. fsigma_in top (topspace top)

⊢ ∀top s t. fsigma_in top s ∧ fsigma_in top t ⇒ fsigma_in top (s ∪ t)

⊢ ∀top t.
    countable t ∧ (∀s. s ∈ t ⇒ fsigma_in top s) ⇒
    fsigma_in top (BIGUNION t)

⊢ ∀top s.
    gdelta_in top s ⇔
    s ⊆ topspace top ∧ (countable INTERSECTION_OF open_in top) s

⊢ ∀top s.
    gdelta_in top s ⇔
    ∃c. (∀n. open_in top (c n)) ∧ (∀n. c (n + 1) ⊆ c n) ∧
        BIGINTER {c n | n ∈ 𝕌(:num)} = s

⊢ ∀top s t. gdelta_in top s ∧ fsigma_in top t ⇒ gdelta_in top (s DIFF t)

⊢ ∀top. gdelta_in top ∅

⊢ ∀top s.
    gdelta_in top s ⇔
    s ⊆ topspace top ∧ fsigma_in top (topspace top DIFF s)

⊢ ∀top s t.
    gdelta_in top s ⇒
    (gdelta_in (subtopology top s) t ⇔ gdelta_in top t ∧ t ⊆ s)

⊢ ∀top s t. gdelta_in top s ∧ gdelta_in top t ⇒ gdelta_in top (s ∩ t)

⊢ ∀top t.
    countable t ∧ t ≠ ∅ ∧ (∀s. s ∈ t ⇒ gdelta_in top s) ⇒
    gdelta_in top (BIGINTER t)

⊢ ∀top s. gdelta_in top relative_to s = gdelta_in (subtopology top s)

⊢ ∀top s. gdelta_in top s ⇒ s ⊆ topspace top

⊢ ∀top u s.
    gdelta_in (subtopology top u) s ⇔ ∃t. gdelta_in top t ∧ s = t ∩ u

⊢ ∀top. gdelta_in top (topspace top)

⊢ ∀top s t. gdelta_in top s ∧ gdelta_in top t ⇒ gdelta_in top (s ∪ t)

⊢ ∀m x y r.
    y ∈ mball m (x,r) ⇔ x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) < r

⊢ ∀m x r y.
    y ∈ mcball m (x,r) ⇔ x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) ≤ r

⊢ ismet (λ(x,y). abs (y − x))

⊢ ismet (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))

⊢ ∀m. istopology
        {u | u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u}

⊢ ∀top1 top2 top3 f g.
    Lipschitz_continuous_map (top1,top2) f ∧
    Lipschitz_continuous_map (top2,top3) g ⇒
    Lipschitz_continuous_map (top1,top3) (g ∘ f)

⊢ ∀E1 E2 c. Lipschitz_continuous_map (E1,E2) (λx. c)

⊢ ∀E1 E2 f.
    Lipschitz_continuous_map (E1,E2) f ⇔
    ∃k. 0 < k ∧ ∀x y. dist E2 (f x,f y) ≤ k * dist E1 (x,y)

⊢ ∀E A e.
    0 < e ⇒
    ∃f. Lipschitz_continuous_map (E,mr1) f ∧ (∀x. 0 ≤ f x ∧ f x ≤ 1) ∧
        (∀x. x ∈ A ⇒ f x = 1) ∧ ∀x. e ≤ set_dist E ({x},A) ⇒ f x = 0

⊢ ∀E1 E2 f.
    Lipschitz_continuous_map (E1,E2) f ⇒ continuous_map (mtop E1,mtop E2) f

⊢ ∀E s. Lipschitz_continuous_map (E,mr1) (λx. set_dist E ({x},s))

⊢ ∀m x r. r ≤ 0 ⇒ mball m (x,r) = ∅

⊢ ∀m x r. mball m (x,r) ⊆ mcball m (x,r)

⊢ ∀m x r. mball m (x,r) ⊆ mspace m

⊢ ∀m x r. r < 0 ⇒ mcball m (x,r) = ∅

⊢ ∀m x r. x ∉ mspace m ⇒ mcball m (x,r) = ∅

⊢ ∀m x r. mcball m (x,r) = ∅ ⇔ x ∉ mspace m ∨ r < 0

⊢ ∀m x e. e = 0 ⇒ mcball m (x,e) = {x}

⊢ ∀m x y a b.
    y ∈ mspace m ∧ dist m (x,y) + a ≤ b ⇒ mcball m (x,a) ⊆ mcball m (y,b)

⊢ ∀m x a b. a ≤ b ⇒ mcball m (x,a) ⊆ mcball m (x,b)

⊢ ∀m x r. mcball m (x,r) ⊆ mspace m

⊢ ∀m x. mcball m (x,0) = {x}

⊢ ∀m x y. dist m (x,y) = 0 ⇔ x = y

⊢ ∀m x y. dist m (x,y) ≤ 0 ⇔ dist m (x,y) = 0

⊢ ∀m x y. 0 < dist m (x,y) ⇔ x ≠ y

⊢ ∀m x y. 0 ≤ dist m (x,y)

⊢ ∀m x y. x ≠ y ⇒ 0 < dist m (x,y)

⊢ ∀m x. dist m (x,x) = 0

⊢ ∀m x y. dist m (x,y) = dist m (y,x)

⊢ ∀m x y z. dist m (x,z) ≤ dist m (x,y) + dist m (y,z)

⊢ ∀m x y z. dist m (x,y) − dist m (y,z) ≤ dist m (x,z)

⊢ ∀m m' f.
    continuous_map (mtop m,mtop m') f ⇔
    (∀x. x ∈ mspace m ⇒ f x ∈ mspace m') ∧
    ∀a e.
      0 < e ∧ a ∈ mspace m ⇒
      ∃d. 0 < d ∧
          ∀x. x ∈ mspace m ∧ dist m (a,x) < d ⇒ dist m' (f a,f x) < e

⊢ ∀m. ismet (dist m)

⊢ ∀m x y. x ≠ y ⇒ 0 < dist m (x,y)

⊢ ∀m x y. 0 ≤ dist m (x,y)

⊢ ∀m x. dist m (x,x) = 0

⊢ ∀m x y. dist m (x,y) = dist m (y,x)

⊢ ∀m x y z. dist m (x,z) ≤ dist m (x,y) + dist m (y,z)

⊢ ∀m x y. dist m (x,y) = 0 ⇔ x = y

⊢ ∀m. metrizable_space (mtop m)

⊢ ∀x d. dist mr1 (x,x + d) = abs d

⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x + d) = d

⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x + d) = d

⊢ ∀x y z. x < z ∧ dist mr1 (x,y) < z − x ⇒ y < z

⊢ ∀x y. dist mr1 (x,y) = abs (y − x)

⊢ ∀x. limpt (mtop mr1) x 𝕌(:real)

⊢ ∀x d. dist mr1 (x,x − d) = abs d

⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x − d) = d

⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x − d) = d

⊢ ∀x1 x2 y1 y2. dist mr2 ((x1,x2),y1,y2) = sqrt ((x1 − y1)² + (x2 − y2)²)

⊢ ∀x1 x2 y1 y2. dist mr2 ((-x1,-x2),-y1,-y2) = dist mr2 ((x1,x2),y1,y2)

⊢ ∀m. mspace m = 𝕌(:α)

⊢ ∀m x S'.
    limpt (mtop m) x S' ⇔ ∀e. 0 < e ⇒ ∃y. x ≠ y ∧ S' y ∧ dist m (x,y) < e

⊢ ∀m x s.
    limpt (mtop m) x s ⇔ ∀e. 0 < e ⇒ ∃y. x ≠ y ∧ y ∈ s ∧ dist m (x,y) < e

⊢ ∀S' m.
    open_in (mtop m) S' ⇔
    ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y

⊢ ∀m s.
    open_in (mtop m) s ⇔
    ∀x. x ∈ s ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ y ∈ s

⊢ ∀top s. metrizable_space top ∧ open_in top s ⇒ fsigma_in top s

⊢ ∀top s. open_in top s ⇒ gdelta_in top s

⊢ ∀m x r. open_in (mtop m) (mball m (x,r))

⊢ ∀m u.
    open_in (mtop m) u ⇔
    u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u

⊢ ∀x e. 0 ≤ e ⇒ ∃y. dist (x,y) = e

⊢ ∀s t d.
    s ≠ ∅ ∧ t ≠ ∅ ∧ (∀x y. x ∈ s ∧ y ∈ t ⇒ d ≤ dist m (x,y)) ⇒
    d ≤ set_dist m (s,t)

⊢ ∀d s t.
    d ≤ set_dist m (s,t) ⇔
    (∀x y. x ∈ s ∧ y ∈ t ⇒ d ≤ dist m (x,y)) ∧ (s = ∅ ∨ t = ∅ ⇒ d ≤ 0)

⊢ ∀s t b.
    s ≠ ∅ ∧ t ≠ ∅ ∧ set_dist m (s,t) < b ⇒
    ∃x y. x ∈ s ∧ y ∈ t ∧ dist m (x,y) < b

⊢ (∀t. set_dist m (∅,t) = 0) ∧ ∀s. set_dist m (s,∅) = 0

⊢ ∀s x. closed_in (mtop m) s ⇒ (set_dist m ({x},s) = 0 ⇔ s = ∅ ∨ x ∈ s)

⊢ ∀s t x y. x ∈ s ∧ y ∈ t ⇒ set_dist m (s,t) ≤ dist m (x,y)

⊢ ∀s t x. x ∈ s ⇒ set_dist m (s,t) ≤ set_dist m ({x},t)

⊢ ∀s x y. abs (set_dist m ({x},s) − set_dist m ({y},s)) ≤ dist m (x,y)

⊢ ∀s t. 0 ≤ set_dist m (s,t)

⊢ ∀s. set_dist m (s,s) = 0

⊢ ∀x y. set_dist m ({x},{y}) = dist m (x,y)

⊢ ∀x s. x ∈ s ⇒ set_dist m ({x},s) = 0

⊢ ∀s t s' t'.
    s' ⊆ s ∧ t' ⊆ t ∧
    (∀x y.
       x ∈ s ∧ y ∈ t ⇒
       ∃x' y'. x' ∈ s' ∧ y' ∈ t' ∧ dist m (x',y') ≤ dist m (x,y)) ⇒
    set_dist m (s',t') = set_dist m (s,t)

⊢ ∀s t u. s ≠ ∅ ∧ s ⊆ t ⇒ set_dist m (t,u) ≤ set_dist m (s,u)

⊢ ∀s t u. t ≠ ∅ ∧ t ⊆ u ⇒ set_dist m (s,u) ≤ set_dist m (s,t)

⊢ ∀s t. set_dist m (s,t) = set_dist m (t,s)

⊢ ∀s a t. set_dist m (s,t) ≤ set_dist m (s,{a}) + set_dist m ({a},t)

⊢ ∀s t a b d.
    a ∈ s ∧ b ∈ t ∧ dist m (a,b) = d ∧
    (∀x y. x ∈ s ∧ y ∈ t ⇒ dist m (a,b) ≤ dist m (x,y)) ⇒
    set_dist m (s,t) = d

⊢ (∀s. set_dist m (s,𝕌(:α)) = 0) ∧ ∀t. set_dist m (𝕌(:α),t) = 0

⊢ ∀s t. ¬DISJOINT s t ⇒ set_dist m (s,t) = 0

⊢ topspace (mtop m) = 𝕌(:α)

⊢ ∀m. topspace (mtop m) = mspace m

⊢ ∀m x y. dist m (x,y) / (1 + dist m (x,y)) = 1 − (1 + dist m (x,y))⁻¹

⊢ ∀m. ismet (λ(x,y). dist m (x,y) / (1 + dist m (x,y)))

⊢ ∀m x y. dist (bounded_metric m) (x,y) < 1

⊢ ∀m x y. dist (bounded_metric m) (x,y) = dist m (x,y) / (1 + dist m (x,y))

⊢ ∀m s e. closed_in (mtop m) (set_mcball m s e)

⊢ ∀x y. dist (x,y) = abs (x − y)

⊢ ∀m x r.
    mball m (x,r) = {y | x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) < r}

⊢ ∀m. istopology (λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)

⊢ ∀m. mtop m =
      topology
        {u | u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u}