# Structure metricTheory

Source File Identifier index Theory binding index

```signature metricTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val ball : thm
val ismet : thm
val metric_TY_DEF : thm
val metric_tybij : thm
val mr1 : thm
val mtop : thm

(*  Theorems  *)
val BALL_NEIGH : thm
val BALL_OPEN : thm
val ISMET_R1 : 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 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 MTOP_LIMPT : thm
val MTOP_OPEN : thm
val mtop_istopology : thm

val metric_grammars : type_grammar.grammar * term_grammar.grammar
(*
[real] Parent theory of "metric"

[topology] Parent theory of "metric"

[ball]  Definition

⊢ ∀m x e. metric\$B m (x,e) = (λy. dist m (x,y) < e)

[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)

[metric_TY_DEF]  Definition

⊢ ∃rep. TYPE_DEFINITION ismet rep

[metric_tybij]  Definition

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

[mr1]  Definition

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

[mtop]  Definition

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

[BALL_NEIGH]  Theorem

⊢ ∀m x e. 0 < e ⇒ neigh (mtop m) (metric\$B m (x,e),x)

[BALL_OPEN]  Theorem

⊢ ∀m x e. 0 < e ⇒ open_in (mtop m) (metric\$B m (x,e))

[ISMET_R1]  Theorem

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

[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)

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

[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)

[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

[mtop_istopology]  Theorem

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

*)
end

```

Source File Identifier index Theory binding index