Theory "metric"

Signature

Definitions

mtop

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

mr1

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

metric_tybij

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

metric_TY_DEF

⊢ ∃rep. TYPE_DEFINITION ismet rep

ismet

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

ball

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

Theorems

MTOP_OPEN

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

MTOP_LIMPT

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

mtop_istopology

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

MR1_SUB_LT

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

MR1_SUB_LE

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

MR1_SUB

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

MR1_LIMPT

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

MR1_DEF

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

MR1_BETWEEN1

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

MR1_ADD_POS

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

MR1_ADD_LT

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

MR1_ADD

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

METRIC_ZERO

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

METRIC_TRIANGLE

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

METRIC_SYM

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

METRIC_SAME

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

METRIC_POS

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

METRIC_NZ

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

METRIC_ISMET

⊢ ∀m. ismet (dist m)

ISMET_R1

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

BALL_OPEN

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

BALL_NEIGH

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