Theory "topology"

Parents     real

Signature

Type Arity
metric 1
topology 1
Constant Type
B :α metric -> α # real -> α -> bool
closed :α topology -> (α -> bool) -> bool
dist :α metric -> α # α -> real
ismet :(α # α -> real) -> bool
istopology :((α -> bool) -> bool) -> bool
limpt :α topology -> α -> (α -> bool) -> bool
metric :(α # α -> real) -> α metric
mr1 :real metric
mtop :α metric -> α topology
neigh :α topology -> (α -> bool) # α -> bool
open :α topology -> (α -> bool) -> bool
re_intersect :(α -> bool) -> (α -> bool) -> α -> bool
re_union :(α -> bool) -> (α -> bool) -> α -> bool
topology :((α -> bool) -> bool) -> α topology

Definitions

re_union 
⊢ ∀P Q. P re_union Q = (λx. P x ∨ Q x)
re_intersect 
⊢ ∀P Q. P re_intersect Q = (λx. P x ∧ Q x)
istopology 
⊢ ∀L.
      istopology L ⇔
      L ∅ ∧ L 𝕌(:α) ∧ (∀a b. L a ∧ L b ⇒ L (a re_intersect b)) ∧
      ∀P. P ⊆ L ⇒ L (BIGUNION P)
topology_TY_DEF 
⊢ ∃rep. TYPE_DEFINITION istopology rep
topology_tybij 
⊢ (∀a. topology (open a) = a) ∧ ∀r. istopology r ⇔ open (topology r) = r
neigh 
⊢ ∀top N x. neigh top (N,x) ⇔ ∃P. open top P ∧ P ⊆ N ∧ P x
closed 
⊢ ∀L S'. closed L S' ⇔ open L (COMPL S')
limpt 
⊢ ∀top x S'. limpt top x S' ⇔ ∀N. neigh top (N,x) ⇒ ∃y. x ≠ y ∧ S' y ∧ N y
ismet 
⊢ ∀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 
⊢ ∃rep. TYPE_DEFINITION ismet rep
metric_tybij 
⊢ (∀a. metric (dist a) = a) ∧ ∀r. ismet r ⇔ dist (metric r) = r
mtop 
⊢ ∀m.
      mtop m =
      topology (λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)
ball 
⊢ ∀m x e. topology$B m (x,e) = (λy. dist m (x,y) < e)
mr1 
⊢ mr1 = metric (λ(x,y). abs (y − x))

Theorems

TOPOLOGY 
⊢ ∀L.
      open L ∅ ∧ open L 𝕌(:α) ∧
      (∀x y. open L x ∧ open L y ⇒ open L (x re_intersect y)) ∧
      ∀P. P ⊆ open L ⇒ open L (BIGUNION P)
TOPOLOGY_UNION 
⊢ ∀L P. P ⊆ open L ⇒ open L (BIGUNION P)
OPEN_OWN_NEIGH 
⊢ ∀S' top x. open top S' ∧ S' x ⇒ neigh top (S',x)
OPEN_UNOPEN 
⊢ ∀S' top. open top S' ⇔ BIGUNION {P | open top P ∧ P ⊆ S'} = S'
OPEN_SUBOPEN 
⊢ ∀S' top. open top S' ⇔ ∀x. S' x ⇒ ∃P. P x ∧ open top P ∧ P ⊆ S'
OPEN_NEIGH 
⊢ ∀S' top. open top S' ⇔ ∀x. S' x ⇒ ∃N. neigh top (N,x) ∧ N ⊆ S'
CLOSED_LIMPT 
⊢ ∀top S'. closed top S' ⇔ ∀x. limpt top x S' ⇒ S' x
METRIC_ISMET 
⊢ ∀m. ismet (dist m)
METRIC_ZERO 
⊢ ∀m x y. dist m (x,y) = 0 ⇔ x = y
METRIC_SAME 
⊢ ∀m x. dist m (x,x) = 0
METRIC_POS 
⊢ ∀m x y. 0 ≤ dist m (x,y)
METRIC_SYM 
⊢ ∀m x y. dist m (x,y) = dist m (y,x)
METRIC_TRIANGLE 
⊢ ∀m x y z. dist m (x,z) ≤ dist m (x,y) + dist m (y,z)
METRIC_NZ 
⊢ ∀m x y. x ≠ y ⇒ 0 < dist m (x,y)
mtop_istopology 
⊢ ∀m. istopology (λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)
MTOP_OPEN 
⊢ ∀S' m. open (mtop m) S' ⇔ ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y
BALL_OPEN 
⊢ ∀m x e. 0 < e ⇒ open (mtop m) (topology$B m (x,e))
BALL_NEIGH 
⊢ ∀m x e. 0 < e ⇒ neigh (mtop m) (topology$B m (x,e),x)
MTOP_LIMPT 
⊢ ∀m x S'.
      limpt (mtop m) x S' ⇔ ∀e. 0 < e ⇒ ∃y. x ≠ y ∧ S' y ∧ dist m (x,y) < e
ISMET_R1 
⊢ ismet (λ(x,y). abs (y − x))
MR1_DEF 
⊢ ∀x y. dist mr1 (x,y) = abs (y − x)
MR1_ADD 
⊢ ∀x d. dist mr1 (x,x + d) = abs d
MR1_SUB 
⊢ ∀x d. dist mr1 (x,x − d) = abs d
MR1_ADD_POS 
⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x + d) = d
MR1_SUB_LE 
⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x − d) = d
MR1_ADD_LT 
⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x + d) = d
MR1_SUB_LT 
⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x − d) = d
MR1_BETWEEN1 
⊢ ∀x y z. x < z ∧ dist mr1 (x,y) < z − x ⇒ y < z
MR1_LIMPT 
⊢ ∀x. limpt (mtop mr1) x 𝕌(:real)