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)