namespace http://mathhub.info/MitM/core/topology ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚

theory OpenSetTopology : base:?Logic = 
	include collections?Properties ❙

	prop_isTopology : {G : type} collection G ⟶ prop ❘ 
	  = [G,C] prop_emptyInColl C ∧ prop_fullInColl C ∧ prop_unionInColl C ∧ prop_finiteIntersection C ❘
	  # isTopology 2 ❙
   
	theory topology_theory : base:?Logic > X : type ❘ =
		include typedsets?SetCollection/setColl_theory (X) ❙
		axiom_empty : ⊦ prop_emptyInColl coll ❙
		axiom_full : ⊦ prop_fullInColl coll ❙
		axiom_union : ⊦ prop_unionInColl coll ❙
		axiom_intersection: ⊦ prop_finiteIntersection coll ❙
	❚
	
	topology = [X : type] Mod ☞?OpenSetTopology/topology_theory (X)❙
	topologicalSpace : kind ❘ = {'
		universe : type ,
		topology : topology universe
	'}❙
   
	topologyOf : {G: topologicalSpace} collection (G.universe) ❘ = [G] (G.topology).coll ❘ # topologyOf 1 ❙
   
	isOpen : {G : topologicalSpace} set (G.universe) ⟶ prop ❘ = [G,S] S ∈ (topologyOf G) ❘ # open 2❙
	isClosed : {G : topologicalSpace} set (G.universe) ⟶ prop ❘= [G,S] ((doms G)\ S) ∈ (topologyOf G) ❘ # closed 2❙
	isClopen : {G : topologicalSpace} set (G.universe) ⟶ prop ❘ = [G,S] closed S ∧ open S ❙ 
	
❚


theory coarsefineTopology : base:?Logic = 
  include ?OpenSetTopology ❙
  coarserTopology : {A} collection A ⟶ collection A ⟶ prop ❘ = [A,T1,T2] T1 ⊑ T2 ❙
  finerTopology : {A} collection A ⟶ collection A ⟶ prop ❘ = [A,T1,T2] T2 ⊑ T1 ❙
❚ 

theory TrivialTopology : base:?Logic = 
  include ?OpenSetTopology ❙
  include ☞base:?InformalProofs ❙
  
  trivialTopology : {A : type} collection A ❘ // = [A] setList (set A) ((emptySet A) , ((fullset A) , nil A)) ❘ # trivialTopology 1 ❙
	lemma_empty : {A} ⊦ prop_emptyInColl (trivialTopology A) ❘ = [A] sketch "by construction" ❘ # lemma_empty 1❙
	lemma_full : {A} ⊦ prop_fullInColl (trivialTopology A) ❘ = [A] sketch "by construction" ❘ # lemma_full 1❙
	lemma_union : {A} ⊦ prop_unionInColl (trivialTopology A) ❘ = [A] sketch "by construction" ❘ # lemma_union 1❙
	lemma_intersection: {A} ⊦ prop_finiteIntersection (trivialTopology A) ❘ = [A] sketch "by construction" ❘ # lemma_intersection 1❙

  indiscreteSpace : {A : type} topologicalSpace ❘ // = [A] [' 
      universe := A , 
      topology := trivialTopology A,
      axiom_empty := lemma_empty A,
      axiom_full := lemma_full A,
      (axiom_union) := lemma_union A,
      axiom_intersection := lemma_intersection A
      '] ❙
  // ^ "x.topology" still needs to be the record
  	containing the collection and all the proofs. The topological space only contains the universe and the topology (which is a record itself). ❙
❚

theory DiscreteSpace : base:?Logic =
   include ?OpenSetTopology ❙
   include ☞base:?InformalProofs ❙
   
   discreteTopology : {A} set A ⟶ collection A ❘ = [A,S] ℘ S ❙
 	// lemma_empty : {A : type } ⊦ ∀[S : set A] prop_emptyInColl (discreteTopology S) ❘ = sketch "by construction" ❙
	// lemma_full : ⊦ ∀[S] prop_fullInColl (discreteTopology S) ❘ sketch "by construction" ❙
	// lemma_union : ⊦ ∀[S] prop_unionInColl (discreteTopology S) ❘ sketch "by construction" ❙
	// lemma_intersection: ⊦ ∀[S] prop_finiteIntersection (discreteTopology S) sketch "by construction" ❙
		
    // discreteSpace : {A} set A ⟶ topologicalSpace A ❘ = [A,S] ['
	universe := A, 
	topology := ℘ S 
	axiom_empty := lemma_empty A,
	axiom_full := lemma_full A,
        axiom_union := lemma_union A,
        axiom_intersection := lemma_intersection A
  	'] ❙
   ❚
   
theory ClosureInterior : base:?Logic = 
  include ?OpenSetTopology ❙
   closure : {G : topologicalSpace} set (G.universe) ⟶ set (G.universe) ❘
    = [G,S] ⋃ ⟪ topologyOf G | ([T] closed T ∧ S ⊑ T) ⟫ ([T] T) ❘ # closure 2❙
   interior : {G : topologicalSpace} set (G.universe) ⟶ set (G.universe)❘
    = [G,S] ⋂ ⟪ topologyOf G | ([T] open T ∧ T ⊑ S) ⟫ ([T] T) ❘ # interior 2 ❙
   boundary : {G : topologicalSpace} set (G.universe) ⟶ set (G.universe) ❘
    = [G,S] closure S \ interior S ❘ # boundary 2❙
  ❚                                                             
   
theory Neighborhood : base:?Logic = 
  include ?OpenSetTopology ❙
  neighborhood : {G : topologicalSpace} (G.universe) ⟶ set (G.universe) ⟶ prop ❘
    = [G,a,S] S ∈ topologyOf G ∧ a ∈ S ❘ # neighborhood 3 2❙
  ❚

theory LimitPoint : base:?Logic = 
  include ?Neighborhood ❙
  limitPoint : {G : topologicalSpace} (G.universe) ⟶ set (G.universe) ⟶ prop ❘
    = [G][a,S] S ⊑ doms G ∧ a ∈ S ∧ ∀[N : set (dom G)] neighborhood N a ⇒ ∃[b] b ∈ N ∧ ¬ a ≐ b ❙
  ❚

theory Continuity : base:?Logic = 
  include ?Neighborhood ❙
  include ☞ts:?Functions ❙
  // continuous_def : the preimage of an open set is open ❙
  continuous : {X : topologicalSpace, Y : topologicalSpace} ((dom X) ⟶ (dom Y)) ⟶ prop ❘ 
     = [X,Y,f] ∀[O] O ∈ topologyOf X ⇒ (im f O) ∈ topologyOf Y 
     ❘ # continuous 3 ❙
  continuousAt : {X : topologicalSpace, Y : topologicalSpace} ((dom X) ⟶ (dom Y)) ⟶ (dom X) ⟶ prop ❘ 
     = [X,Y,f,x] ∀[V] neighborhood V (f x) ⇒ neighborhood (preim f V) x
     ❘ # continuousAt 3 4 ❙
  ❚

theory Compactness : base:?Logic = 
  include ?OpenSetTopology ❙
  // compact_def: every open cover C of dom G has a finite subcover D of dom G ❙
  compact : {G : topologicalSpace} prop ❘ = [G] ∀[C] C covers (fullset (G.universe)) ⇒ ∃[D] D subcover C on (fullset (G.universe)) ❘ # compact 1 ❙
  ❚
  
theory TopologyBase : base:?Logic = 
  include ?OpenSetTopology ❙
  base : {X: topologicalSpace}collection (X.universe) ⟶prop ❘ = [G,B] ∀[O] O ∈ topologyOf G ⇒ ∃[C] C ⊑ B ∧ O ≐ UNION C ❘ # 2 basefor 1❙
  ❚
  
theory HausdorffTopology : base:?Logic = 
   include ?OpenSetTopology ❙
   include typedsets?SetRelations ❙
   hausdorffProperty : {G : type}(collection G) ⟶ prop ❘
     = [G,T] ∀[p] ∀ [q] p ∈ (fullset G) ∧ q ∈ (fullset G) ∧ p ≠ q ⇒ 
       ∃[P]∃[Q]P ∈ T ∧ Q ∈ T ∧ p ∈ P ∧ q ∈ Q ∧ disjoint P Q ❘ role abbreviation ❙
       
   theory hausdorff_theory : base:?Logic > X : type ❘ =
   	 include ?OpenSetTopology/topology_theory (X) ❙
   	 ishausdorff : ⊦ hausdorffProperty X coll ❙
   ❚
   hausdorffTopology : type ⟶ type ❘ = [X : type] Mod ☞?HausdorffTopology/hausdorff_theory (X) ❙
   
   hausdorffSpace : kind ❘= {'
		universe : type ,
		topology : hausdorffTopology universe
	'} ❙
❚