Structure metricTheory
signature metricTheory =
sig
type thm = Thm.thm
(* Definitions *)
val Lipschitz_condition_def : thm
val Lipschitz_continuous_map : thm
val ball : thm
val bounded_metric_def : thm
val dist_def : thm
val fsigma_in : thm
val gdelta_in : thm
val ismet : thm
val mcball : thm
val metric_TY_DEF : thm
val metric_tybij : thm
val metrizable_space : thm
val mr1 : thm
val mr2 : thm
val mspace : thm
val mtop : thm
val set_dist_def : thm
(* Theorems *)
val BALL_NEIGH : thm
val BALL_OPEN : thm
val CENTRE_IN_MBALL : thm
val CENTRE_IN_MBALL_EQ : thm
val CENTRE_IN_MCBALL : thm
val CENTRE_IN_MCBALL_EQ : thm
val CLOSED_IMP_FSIGMA_IN : thm
val CLOSED_IMP_GDELTA_IN : thm
val CLOSED_IN_MCBALL : thm
val CLOSED_IN_METRIC : thm
val CONTINUOUS_MAP_FROM_METRIC : thm
val CONTINUOUS_MAP_TO_METRIC : thm
val DIST_0 : thm
val DIST_EQ : thm
val DIST_EQ_0 : thm
val DIST_LE_0 : thm
val DIST_MUL : thm
val DIST_NZ : thm
val DIST_POS_LE : thm
val DIST_POS_LT : thm
val DIST_REFL : thm
val DIST_SYM : thm
val DIST_TRIANGLE : thm
val DIST_TRIANGLE_ADD : thm
val DIST_TRIANGLE_ADD_HALF : thm
val DIST_TRIANGLE_ALT : thm
val DIST_TRIANGLE_HALF_L : thm
val DIST_TRIANGLE_HALF_R : thm
val DIST_TRIANGLE_LE : thm
val DIST_TRIANGLE_LT : thm
val EXISTS_METRIZABLE_SPACE : thm
val FORALL_METRIC_TOPOLOGY : thm
val FORALL_METRIZABLE_SPACE : thm
val FORALL_POS_MONO : thm
val FORALL_POS_MONO_1 : thm
val FORALL_POS_MONO_1_EQ : thm
val FORALL_POS_MONO_EQ : thm
val FORALL_SUC : thm
val FSIGMA_IN_ASCENDING : thm
val FSIGMA_IN_DIFF : thm
val FSIGMA_IN_EMPTY : thm
val FSIGMA_IN_FSIGMA_SUBTOPOLOGY : thm
val FSIGMA_IN_GDELTA_IN : thm
val FSIGMA_IN_INTER : thm
val FSIGMA_IN_RELATIVE_TO : thm
val FSIGMA_IN_RELATIVE_TO_TOPSPACE : thm
val FSIGMA_IN_SUBSET : thm
val FSIGMA_IN_SUBTOPOLOGY : thm
val FSIGMA_IN_TOPSPACE : thm
val FSIGMA_IN_UNION : thm
val FSIGMA_IN_UNIONS : thm
val GDELTA_IN_ALT : thm
val GDELTA_IN_DESCENDING : thm
val GDELTA_IN_DIFF : thm
val GDELTA_IN_EMPTY : thm
val GDELTA_IN_FSIGMA_IN : thm
val GDELTA_IN_GDELTA_SUBTOPOLOGY : thm
val GDELTA_IN_INTER : thm
val GDELTA_IN_INTERS : thm
val GDELTA_IN_RELATIVE_TO : thm
val GDELTA_IN_SUBSET : thm
val GDELTA_IN_SUBTOPOLOGY : thm
val GDELTA_IN_TOPSPACE : thm
val GDELTA_IN_UNION : thm
val IN_MBALL : thm
val IN_MCBALL : thm
val ISMET_R1 : thm
val ISMET_R2 : thm
val IS_TOPOLOGY_METRIC_TOPOLOGY : thm
val Lipschitz_continuous_map_def : thm
val Lipschitz_continuous_map_exists : thm
val Lipschitz_continuous_map_imp_continuous_map : thm
val Lipschitz_continuous_map_set_dist : thm
val MBALL_EMPTY : thm
val MBALL_SUBSET_MCBALL : thm
val MBALL_SUBSET_MSPACE : thm
val MCBALL_EMPTY : thm
val MCBALL_EMPTY_ALT : thm
val MCBALL_EQ_EMPTY : thm
val MCBALL_SUBSET : thm
val MCBALL_SUBSET_CONCENTRIC : thm
val MCBALL_SUBSET_MSPACE : thm
val MDIST_EQ_0 : thm
val MDIST_POS_LE : thm
val MDIST_REFL : thm
val MDIST_SYM : thm
val MDIST_TRIANGLE : thm
val MDIST_TRIANGLE_SUB : thm
val METRIC_CONTINUOUS_MAP : thm
val METRIC_ISMET : thm
val METRIC_NZ : thm
val METRIC_POS : thm
val METRIC_SAME : thm
val METRIC_SYM : thm
val METRIC_TRIANGLE : thm
val METRIC_ZERO : thm
val METRIZABLE_SPACE_MTOPOLOGY : thm
val MR1_ADD : thm
val MR1_ADD_LT : thm
val MR1_ADD_POS : thm
val MR1_BETWEEN1 : thm
val MR1_DEF : thm
val MR1_LIMPT : thm
val MR1_SUB : thm
val MR1_SUB_LE : thm
val MR1_SUB_LT : thm
val MR2_DEF : thm
val MR2_MIRROR : thm
val MTOP_LIMPT : thm
val MTOP_OPEN : thm
val OPEN_IMP_FSIGMA_IN : thm
val OPEN_IMP_GDELTA_IN : thm
val OPEN_IN_MBALL : thm
val OPEN_IN_MTOPOLOGY : thm
val REAL_CHOOSE_DIST : thm
val REAL_LE_SET_DIST : thm
val REAL_LE_SET_DIST_EQ : thm
val REAL_SET_DIST_LT_EXISTS : thm
val SET_DIST_EMPTY : thm
val SET_DIST_EQ_0_CLOSED : thm
val SET_DIST_LE_DIST : thm
val SET_DIST_LE_SING : thm
val SET_DIST_LIPSCHITZ : thm
val SET_DIST_POS_LE : thm
val SET_DIST_REFL : thm
val SET_DIST_SINGS : thm
val SET_DIST_SING_IN_SET : thm
val SET_DIST_SUBSETS_EQ : thm
val SET_DIST_SUBSET_LEFT : thm
val SET_DIST_SUBSET_RIGHT : thm
val SET_DIST_SYM : thm
val SET_DIST_TRIANGLE : thm
val SET_DIST_UNIQUE : thm
val SET_DIST_UNIV : thm
val SET_DIST_ZERO : thm
val TOPSPACE_MTOP : thm
val TOPSPACE_MTOPOLOGY : thm
val bounded_metric_alt : thm
val bounded_metric_ismet : thm
val bounded_metric_lt_1 : thm
val bounded_metric_thm : thm
val dist : thm
val mball : thm
val mtop_istopology : thm
val mtopology : thm
(*
[real_sigma] Parent theory of "metric"
[topology] Parent theory of "metric"
[Lipschitz_condition_def] Definition
⊢ ∀E1 E2 k f.
Lipschitz_condition (E1,E2) k f ⇔
∀x y. dist E2 (f x,f y) ≤ k * dist E1 (x,y)
[Lipschitz_continuous_map] Definition
⊢ ∀E1 E2 f.
Lipschitz_continuous_map (E1,E2) f ⇔
∃k. 0 < k ∧ Lipschitz_condition (E1,E2) k f
[ball] Definition
⊢ ∀m x e. mball m (x,e) = (λy. dist m (x,y) < e)
[bounded_metric_def] Definition
⊢ ∀m. bounded_metric m =
metric (λ(x,y). dist m (x,y) / (1 + dist m (x,y)))
[dist_def] Definition
⊢ dist = dist mr1
[fsigma_in] Definition
⊢ ∀top. fsigma_in top = countable UNION_OF closed_in top
[gdelta_in] Definition
⊢ ∀top.
gdelta_in top =
countable INTERSECTION_OF open_in top relative_to topspace top
[ismet] Definition
⊢ ∀m. ismet m ⇔
(∀x y. m (x,y) = 0 ⇔ x = y) ∧
∀x y z. m (y,z) ≤ m (x,y) + m (x,z)
[mcball] Definition
⊢ ∀m x r.
mcball m (x,r) =
{y | x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) ≤ r}
[metric_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION ismet rep
[metric_tybij] Definition
⊢ (∀a. metric (dist a) = a) ∧ ∀r. ismet r ⇔ dist (metric r) = r
[metrizable_space] Definition
⊢ ∀top. metrizable_space top ⇔ ∃m. top = mtop m
[mr1] Definition
⊢ mr1 = metric (λ(x,y). abs (y − x))
[mr2] Definition
⊢ mr2 = metric (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))
[mspace] Definition
⊢ ∀m. mspace m = topspace (mtop m)
[mtop] Definition
⊢ ∀m. mtop m =
topology
(λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)
[set_dist_def] Definition
⊢ ∀d s t.
set_dist d (s,t) =
if s = ∅ ∨ t = ∅ then 0 else inf {dist d (x,y) | x ∈ s ∧ y ∈ t}
[BALL_NEIGH] Theorem
⊢ ∀m x e. 0 < e ⇒ neigh (mtop m) (mball m (x,e),x)
[BALL_OPEN] Theorem
⊢ ∀m x e. 0 < e ⇒ open_in (mtop m) (mball m (x,e))
[CENTRE_IN_MBALL] Theorem
⊢ ∀m x r. 0 < r ∧ x ∈ mspace m ⇒ x ∈ mball m (x,r)
[CENTRE_IN_MBALL_EQ] Theorem
⊢ ∀m x r. x ∈ mball m (x,r) ⇔ x ∈ mspace m ∧ 0 < r
[CENTRE_IN_MCBALL] Theorem
⊢ ∀m x r. 0 ≤ r ∧ x ∈ mspace m ⇒ x ∈ mcball m (x,r)
[CENTRE_IN_MCBALL_EQ] Theorem
⊢ ∀m x r. x ∈ mcball m (x,r) ⇔ x ∈ mspace m ∧ 0 ≤ r
[CLOSED_IMP_FSIGMA_IN] Theorem
⊢ ∀top s. closed_in top s ⇒ fsigma_in top s
[CLOSED_IMP_GDELTA_IN] Theorem
⊢ ∀top s. metrizable_space top ∧ closed_in top s ⇒ gdelta_in top s
[CLOSED_IN_MCBALL] Theorem
⊢ ∀m x r. closed_in (mtop m) (mcball m (x,r))
[CLOSED_IN_METRIC] Theorem
⊢ ∀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))
[CONTINUOUS_MAP_FROM_METRIC] Theorem
⊢ ∀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
[CONTINUOUS_MAP_TO_METRIC] Theorem
⊢ ∀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)
[DIST_0] Theorem
⊢ ∀x. dist (x,0) = abs x ∧ dist (0,x) = abs x
[DIST_EQ] Theorem
⊢ ∀w x y z. dist (w,x) = dist (y,z) ⇔ (dist (w,x))² = (dist (y,z))²
[DIST_EQ_0] Theorem
⊢ ∀x y. dist (x,y) = 0 ⇔ x = y
[DIST_LE_0] Theorem
⊢ ∀x y. dist (x,y) ≤ 0 ⇔ x = y
[DIST_MUL] Theorem
⊢ ∀x y c. dist (c * x,c * y) = abs c * dist (x,y)
[DIST_NZ] Theorem
⊢ ∀x y. x ≠ y ⇔ 0 < dist (x,y)
[DIST_POS_LE] Theorem
⊢ ∀x y. 0 ≤ dist (x,y)
[DIST_POS_LT] Theorem
⊢ ∀x y. x ≠ y ⇒ 0 < dist (x,y)
[DIST_REFL] Theorem
⊢ ∀x. dist (x,x) = 0
[DIST_SYM] Theorem
⊢ ∀x y. dist (x,y) = dist (y,x)
[DIST_TRIANGLE] Theorem
⊢ ∀x y z. dist (x,z) ≤ dist (x,y) + dist (y,z)
[DIST_TRIANGLE_ADD] Theorem
⊢ ∀x x' y y'. dist (x + y,x' + y') ≤ dist (x,x') + dist (y,y')
[DIST_TRIANGLE_ADD_HALF] Theorem
⊢ ∀x x' y y'.
dist (x,x') < e / 2 ∧ dist (y,y') < e / 2 ⇒
dist (x + y,x' + y') < e
[DIST_TRIANGLE_ALT] Theorem
⊢ ∀x y z. dist (y,z) ≤ dist (x,y) + dist (x,z)
[DIST_TRIANGLE_HALF_L] Theorem
⊢ ∀x1 x2 y.
dist (x1,y) < e / 2 ∧ dist (x2,y) < e / 2 ⇒ dist (x1,x2) < e
[DIST_TRIANGLE_HALF_R] Theorem
⊢ ∀x1 x2 y.
dist (y,x1) < e / 2 ∧ dist (y,x2) < e / 2 ⇒ dist (x1,x2) < e
[DIST_TRIANGLE_LE] Theorem
⊢ ∀x y z e. dist (x,z) + dist (y,z) ≤ e ⇒ dist (x,y) ≤ e
[DIST_TRIANGLE_LT] Theorem
⊢ ∀x y z e. dist (x,z) + dist (y,z) < e ⇒ dist (x,y) < e
[EXISTS_METRIZABLE_SPACE] Theorem
⊢ ∀P. (∃top. metrizable_space top ∧ P top (topspace top)) ⇔
∃m. P (mtop m) (mspace m)
[FORALL_METRIC_TOPOLOGY] Theorem
⊢ ∀P. (∀m. P (mtop m) (mspace m)) ⇔
∀top. metrizable_space top ⇒ P top (topspace top)
[FORALL_METRIZABLE_SPACE] Theorem
⊢ ∀P. (∀top. metrizable_space top ⇒ P top (topspace top)) ⇔
∀m. P (mtop m) (mspace m)
[FORALL_POS_MONO] Theorem
⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ∧ (∀n. n ≠ 0 ⇒ P (&n)⁻¹) ⇒
∀e. 0 < e ⇒ P e
[FORALL_POS_MONO_1] Theorem
⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ∧ (∀n. P (&n + 1)⁻¹) ⇒
∀e. 0 < e ⇒ P e
[FORALL_POS_MONO_1_EQ] Theorem
⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ⇒
((∀e. 0 < e ⇒ P e) ⇔ ∀n. P (&n + 1)⁻¹)
[FORALL_POS_MONO_EQ] Theorem
⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ⇒
((∀e. 0 < e ⇒ P e) ⇔ ∀n. n ≠ 0 ⇒ P (&n)⁻¹)
[FORALL_SUC] Theorem
⊢ (∀n. n ≠ 0 ⇒ P n) ⇔ ∀n. P (SUC n)
[FSIGMA_IN_ASCENDING] Theorem
⊢ ∀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
[FSIGMA_IN_DIFF] Theorem
⊢ ∀top s t.
fsigma_in top s ∧ gdelta_in top t ⇒ fsigma_in top (s DIFF t)
[FSIGMA_IN_EMPTY] Theorem
⊢ ∀top. fsigma_in top ∅
[FSIGMA_IN_FSIGMA_SUBTOPOLOGY] Theorem
⊢ ∀top s t.
fsigma_in top s ⇒
(fsigma_in (subtopology top s) t ⇔ fsigma_in top t ∧ t ⊆ s)
[FSIGMA_IN_GDELTA_IN] Theorem
⊢ ∀top s.
fsigma_in top s ⇔
s ⊆ topspace top ∧ gdelta_in top (topspace top DIFF s)
[FSIGMA_IN_INTER] Theorem
⊢ ∀top s t. fsigma_in top s ∧ fsigma_in top t ⇒ fsigma_in top (s ∩ t)
[FSIGMA_IN_RELATIVE_TO] Theorem
⊢ ∀top s. fsigma_in top relative_to s = fsigma_in (subtopology top s)
[FSIGMA_IN_RELATIVE_TO_TOPSPACE] Theorem
⊢ ∀top. fsigma_in top relative_to topspace top = fsigma_in top
[FSIGMA_IN_SUBSET] Theorem
⊢ ∀top s. fsigma_in top s ⇒ s ⊆ topspace top
[FSIGMA_IN_SUBTOPOLOGY] Theorem
⊢ ∀top u s.
fsigma_in (subtopology top u) s ⇔ ∃t. fsigma_in top t ∧ s = t ∩ u
[FSIGMA_IN_TOPSPACE] Theorem
⊢ ∀top. fsigma_in top (topspace top)
[FSIGMA_IN_UNION] Theorem
⊢ ∀top s t. fsigma_in top s ∧ fsigma_in top t ⇒ fsigma_in top (s ∪ t)
[FSIGMA_IN_UNIONS] Theorem
⊢ ∀top t.
countable t ∧ (∀s. s ∈ t ⇒ fsigma_in top s) ⇒
fsigma_in top (BIGUNION t)
[GDELTA_IN_ALT] Theorem
⊢ ∀top s.
gdelta_in top s ⇔
s ⊆ topspace top ∧ (countable INTERSECTION_OF open_in top) s
[GDELTA_IN_DESCENDING] Theorem
⊢ ∀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
[GDELTA_IN_DIFF] Theorem
⊢ ∀top s t.
gdelta_in top s ∧ fsigma_in top t ⇒ gdelta_in top (s DIFF t)
[GDELTA_IN_EMPTY] Theorem
⊢ ∀top. gdelta_in top ∅
[GDELTA_IN_FSIGMA_IN] Theorem
⊢ ∀top s.
gdelta_in top s ⇔
s ⊆ topspace top ∧ fsigma_in top (topspace top DIFF s)
[GDELTA_IN_GDELTA_SUBTOPOLOGY] Theorem
⊢ ∀top s t.
gdelta_in top s ⇒
(gdelta_in (subtopology top s) t ⇔ gdelta_in top t ∧ t ⊆ s)
[GDELTA_IN_INTER] Theorem
⊢ ∀top s t. gdelta_in top s ∧ gdelta_in top t ⇒ gdelta_in top (s ∩ t)
[GDELTA_IN_INTERS] Theorem
⊢ ∀top t.
countable t ∧ t ≠ ∅ ∧ (∀s. s ∈ t ⇒ gdelta_in top s) ⇒
gdelta_in top (BIGINTER t)
[GDELTA_IN_RELATIVE_TO] Theorem
⊢ ∀top s. gdelta_in top relative_to s = gdelta_in (subtopology top s)
[GDELTA_IN_SUBSET] Theorem
⊢ ∀top s. gdelta_in top s ⇒ s ⊆ topspace top
[GDELTA_IN_SUBTOPOLOGY] Theorem
⊢ ∀top u s.
gdelta_in (subtopology top u) s ⇔ ∃t. gdelta_in top t ∧ s = t ∩ u
[GDELTA_IN_TOPSPACE] Theorem
⊢ ∀top. gdelta_in top (topspace top)
[GDELTA_IN_UNION] Theorem
⊢ ∀top s t. gdelta_in top s ∧ gdelta_in top t ⇒ gdelta_in top (s ∪ t)
[IN_MBALL] Theorem
⊢ ∀m x y r.
y ∈ mball m (x,r) ⇔
x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) < r
[IN_MCBALL] Theorem
⊢ ∀m x r y.
y ∈ mcball m (x,r) ⇔
x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) ≤ r
[ISMET_R1] Theorem
⊢ ismet (λ(x,y). abs (y − x))
[ISMET_R2] Theorem
⊢ ismet (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))
[IS_TOPOLOGY_METRIC_TOPOLOGY] Theorem
⊢ ∀m. istopology
{u | u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u}
[Lipschitz_continuous_map_def] Theorem
⊢ ∀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)
[Lipschitz_continuous_map_exists] Theorem
⊢ ∀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
[Lipschitz_continuous_map_imp_continuous_map] Theorem
⊢ ∀E1 E2 f.
Lipschitz_continuous_map (E1,E2) f ⇒
continuous_map (mtop E1,mtop E2) f
[Lipschitz_continuous_map_set_dist] Theorem
⊢ ∀E s. Lipschitz_continuous_map (E,mr1) (λx. set_dist E ({x},s))
[MBALL_EMPTY] Theorem
⊢ ∀m x r. r ≤ 0 ⇒ mball m (x,r) = ∅
[MBALL_SUBSET_MCBALL] Theorem
⊢ ∀m x r. mball m (x,r) ⊆ mcball m (x,r)
[MBALL_SUBSET_MSPACE] Theorem
⊢ ∀m x r. mball m (x,r) ⊆ mspace m
[MCBALL_EMPTY] Theorem
⊢ ∀m x r. r < 0 ⇒ mcball m (x,r) = ∅
[MCBALL_EMPTY_ALT] Theorem
⊢ ∀m x r. x ∉ mspace m ⇒ mcball m (x,r) = ∅
[MCBALL_EQ_EMPTY] Theorem
⊢ ∀m x r. mcball m (x,r) = ∅ ⇔ x ∉ mspace m ∨ r < 0
[MCBALL_SUBSET] Theorem
⊢ ∀m x y a b.
y ∈ mspace m ∧ dist m (x,y) + a ≤ b ⇒
mcball m (x,a) ⊆ mcball m (y,b)
[MCBALL_SUBSET_CONCENTRIC] Theorem
⊢ ∀m x a b. a ≤ b ⇒ mcball m (x,a) ⊆ mcball m (x,b)
[MCBALL_SUBSET_MSPACE] Theorem
⊢ ∀m x r. mcball m (x,r) ⊆ mspace m
[MDIST_EQ_0] Theorem
⊢ ∀m x y. dist m (x,y) = 0 ⇔ x = y
[MDIST_POS_LE] Theorem
⊢ ∀m x y. 0 ≤ dist m (x,y)
[MDIST_REFL] Theorem
⊢ ∀m x. dist m (x,x) = 0
[MDIST_SYM] Theorem
⊢ ∀m x y. dist m (x,y) = dist m (y,x)
[MDIST_TRIANGLE] Theorem
⊢ ∀m x y z. dist m (x,z) ≤ dist m (x,y) + dist m (y,z)
[MDIST_TRIANGLE_SUB] Theorem
⊢ ∀m x y z. dist m (x,y) − dist m (y,z) ≤ dist m (x,z)
[METRIC_CONTINUOUS_MAP] Theorem
⊢ ∀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
[METRIC_ISMET] Theorem
⊢ ∀m. ismet (dist m)
[METRIC_NZ] Theorem
⊢ ∀m x y. x ≠ y ⇒ 0 < dist m (x,y)
[METRIC_POS] Theorem
⊢ ∀m x y. 0 ≤ dist m (x,y)
[METRIC_SAME] Theorem
⊢ ∀m x. dist m (x,x) = 0
[METRIC_SYM] Theorem
⊢ ∀m x y. dist m (x,y) = dist m (y,x)
[METRIC_TRIANGLE] Theorem
⊢ ∀m x y z. dist m (x,z) ≤ dist m (x,y) + dist m (y,z)
[METRIC_ZERO] Theorem
⊢ ∀m x y. dist m (x,y) = 0 ⇔ x = y
[METRIZABLE_SPACE_MTOPOLOGY] Theorem
⊢ ∀m. metrizable_space (mtop m)
[MR1_ADD] Theorem
⊢ ∀x d. dist mr1 (x,x + d) = abs d
[MR1_ADD_LT] Theorem
⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x + d) = d
[MR1_ADD_POS] Theorem
⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x + d) = d
[MR1_BETWEEN1] Theorem
⊢ ∀x y z. x < z ∧ dist mr1 (x,y) < z − x ⇒ y < z
[MR1_DEF] Theorem
⊢ ∀x y. dist mr1 (x,y) = abs (y − x)
[MR1_LIMPT] Theorem
⊢ ∀x. limpt (mtop mr1) x 𝕌(:real)
[MR1_SUB] Theorem
⊢ ∀x d. dist mr1 (x,x − d) = abs d
[MR1_SUB_LE] Theorem
⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x − d) = d
[MR1_SUB_LT] Theorem
⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x − d) = d
[MR2_DEF] Theorem
⊢ ∀x1 x2 y1 y2.
dist mr2 ((x1,x2),y1,y2) = sqrt ((x1 − y1)² + (x2 − y2)²)
[MR2_MIRROR] Theorem
⊢ ∀x1 x2 y1 y2.
dist mr2 ((-x1,-x2),-y1,-y2) = dist mr2 ((x1,x2),y1,y2)
[MTOP_LIMPT] Theorem
⊢ ∀m x S'.
limpt (mtop m) x S' ⇔
∀e. 0 < e ⇒ ∃y. x ≠ y ∧ S' y ∧ dist m (x,y) < e
[MTOP_OPEN] Theorem
⊢ ∀S' m.
open_in (mtop m) S' ⇔
∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y
[OPEN_IMP_FSIGMA_IN] Theorem
⊢ ∀top s. metrizable_space top ∧ open_in top s ⇒ fsigma_in top s
[OPEN_IMP_GDELTA_IN] Theorem
⊢ ∀top s. open_in top s ⇒ gdelta_in top s
[OPEN_IN_MBALL] Theorem
⊢ ∀m x r. open_in (mtop m) (mball m (x,r))
[OPEN_IN_MTOPOLOGY] Theorem
⊢ ∀m u.
open_in (mtop m) u ⇔
u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u
[REAL_CHOOSE_DIST] Theorem
⊢ ∀x e. 0 ≤ e ⇒ ∃y. dist (x,y) = e
[REAL_LE_SET_DIST] Theorem
⊢ ∀s t d.
s ≠ ∅ ∧ t ≠ ∅ ∧ (∀x y. x ∈ s ∧ y ∈ t ⇒ d ≤ dist m (x,y)) ⇒
d ≤ set_dist m (s,t)
[REAL_LE_SET_DIST_EQ] Theorem
⊢ ∀d s t.
d ≤ set_dist m (s,t) ⇔
(∀x y. x ∈ s ∧ y ∈ t ⇒ d ≤ dist m (x,y)) ∧
(s = ∅ ∨ t = ∅ ⇒ d ≤ 0)
[REAL_SET_DIST_LT_EXISTS] Theorem
⊢ ∀s t b.
s ≠ ∅ ∧ t ≠ ∅ ∧ set_dist m (s,t) < b ⇒
∃x y. x ∈ s ∧ y ∈ t ∧ dist m (x,y) < b
[SET_DIST_EMPTY] Theorem
⊢ (∀t. set_dist m (∅,t) = 0) ∧ ∀s. set_dist m (s,∅) = 0
[SET_DIST_EQ_0_CLOSED] Theorem
⊢ ∀s x.
closed_in (mtop m) s ⇒ (set_dist m ({x},s) = 0 ⇔ s = ∅ ∨ x ∈ s)
[SET_DIST_LE_DIST] Theorem
⊢ ∀s t x y. x ∈ s ∧ y ∈ t ⇒ set_dist m (s,t) ≤ dist m (x,y)
[SET_DIST_LE_SING] Theorem
⊢ ∀s t x. x ∈ s ⇒ set_dist m (s,t) ≤ set_dist m ({x},t)
[SET_DIST_LIPSCHITZ] Theorem
⊢ ∀s t x y.
abs (set_dist m ({x},s) − set_dist m ({y},s)) ≤ dist m (x,y)
[SET_DIST_POS_LE] Theorem
⊢ ∀s t. 0 ≤ set_dist m (s,t)
[SET_DIST_REFL] Theorem
⊢ ∀s. set_dist m (s,s) = 0
[SET_DIST_SINGS] Theorem
⊢ ∀x y. set_dist m ({x},{y}) = dist m (x,y)
[SET_DIST_SING_IN_SET] Theorem
⊢ ∀x s. x ∈ s ⇒ set_dist m ({x},s) = 0
[SET_DIST_SUBSETS_EQ] Theorem
⊢ ∀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)
[SET_DIST_SUBSET_LEFT] Theorem
⊢ ∀s t u. s ≠ ∅ ∧ s ⊆ t ⇒ set_dist m (t,u) ≤ set_dist m (s,u)
[SET_DIST_SUBSET_RIGHT] Theorem
⊢ ∀s t u. t ≠ ∅ ∧ t ⊆ u ⇒ set_dist m (s,u) ≤ set_dist m (s,t)
[SET_DIST_SYM] Theorem
⊢ ∀s t. set_dist m (s,t) = set_dist m (t,s)
[SET_DIST_TRIANGLE] Theorem
⊢ ∀s a t. set_dist m (s,t) ≤ set_dist m (s,{a}) + set_dist m ({a},t)
[SET_DIST_UNIQUE] Theorem
⊢ ∀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
[SET_DIST_UNIV] Theorem
⊢ (∀s. set_dist m (s,𝕌(:α)) = 0) ∧ ∀t. set_dist m (𝕌(:α),t) = 0
[SET_DIST_ZERO] Theorem
⊢ ∀s t. ¬DISJOINT s t ⇒ set_dist m (s,t) = 0
[TOPSPACE_MTOP] Theorem
⊢ topspace (mtop m) = 𝕌(:α)
[TOPSPACE_MTOPOLOGY] Theorem
⊢ ∀m. topspace (mtop m) = mspace m
[bounded_metric_alt] Theorem
⊢ ∀m x y.
dist m (x,y) / (1 + dist m (x,y)) = 1 − (1 + dist m (x,y))⁻¹
[bounded_metric_ismet] Theorem
⊢ ∀m. ismet (λ(x,y). dist m (x,y) / (1 + dist m (x,y)))
[bounded_metric_lt_1] Theorem
⊢ ∀m x y. dist (bounded_metric m) (x,y) < 1
[bounded_metric_thm] Theorem
⊢ ∀m x y.
dist (bounded_metric m) (x,y) = dist m (x,y) / (1 + dist m (x,y))
[dist] Theorem
⊢ ∀x y. dist (x,y) = abs (x − y)
[mball] Theorem
⊢ ∀m x r.
mball m (x,r) =
{y | x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) < r}
[mtop_istopology] Theorem
⊢ ∀m. istopology
(λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)
[mtopology] Theorem
⊢ ∀m. mtop m =
topology
{u | u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u}
*)
end
HOL 4, Trindemossen-2