namespace latin:/❚

fixmeta latin:/powertypes?PowerSFOL❚

theory ClosureSystem =
  X  : tp❙
  CC : tm ℘℘X❙
  
  intersection : {Q: tm ℘℘X} ⊦ Q ⊆ CC ⟶ ⊦ (⋂ Q) ∈ CC❙
  // provable ❙
  full_closed  : ⊦ fullset ∈ CC❙
❚

theory ClosureOperator =
  X       : tp❙
  closure : tm ℘X ⟶ tm ℘X❘ # cl 1 prec 50❙
  
  extensive    : {A} ⊦ A ⊆ cl A❙
  monotone     : {A,B} ⊦ A ⊆ B ⟶ ⊦ cl A ⊆ cl B❙
  idempotent   : {A} ⊦ cl (cl A) ≐ cl A❙
❚

theory InteriorTopology = 
	X : tp ❙
	interior : tm ℘X ⟶ tm ℘X❙

	int_extensivity : {A} ⊦ ( subset X (interior A) A)❙
	idempotence : {A} ⊦ ((interior A) ≐  (interior (interior A)))❙
	bin_inters : {A, B} ⊦ ((interior (A ∩ B)) ≐ ((interior A) ∩ (interior B)))❙
	preservation : ⊦ ((interior (full X)) ≐ (full X))❙
	
❚

theory ClosureTopology =
  include ?ClosureOperator❙

  closure_empty  : ⊦ cl (empty X) ≐ (empty X)❙
  closure_union  : {A,B} ⊦ cl (A ∪ B) ≐ cl A ∪ cl B❙
  
  // monotone provable from union❙ 
❚

//   isomorphic to ClosureOperator❚
theory Closeness =
  X     : tp❙
  close : tm X ⟶ tm ℘X ⟶ prop❘ # 1 | 2 prec 40❙

  in_close     : {x,A} ⊦ x ∈ A ⟶ ⊦ x|A❙
  bigger_close : {x,A,B} ⊦ x|A ⟶ ⊦ A ⊆ B ⟶ ⊦ x|B❙
  transitive   : {A,B,x} ⊦ x|B ⟶ ⊦ (∀ [y] y ∈ B ⇒ y|A) ⟶ ⊦ x|A❙
❚
  
theory ClosenessTopology =
  include ?Closeness❙

  empty_union  : {x} ⊦ ¬ x|(empty X)❙
  finite_union : {x,A,B} ⊦ x|(A ∪ B) ⟶ ⊦ x|A ∨ x|B❙
  
  // bigger_close provable from union ❙
❚

//   empty and full axioms are implied by/correspond to empty union and empty intersection❚
theory OpenTopology =
  X     : tp❙
  OO    : tm ℘℘X❙
  
  full_open  : ⊦ (full X) ∈ OO❙
  union_open : {Q: tm ℘℘X} ⊦ Q ⊆ OO ⟶ ⊦ (⋃ Q) ∈ OO❙

  empty_open : ⊦ (empty X) ∈ OO ❙
  finite_intersection : {A,B} ⊦ A ∈ OO ⟶ ⊦ B ∈ OO ⟶ ⊦ A ∩ B ∈ OO❙
❚

theory ClosedTopology =
  include ?ClosureSystem❙  
  empty_closed : ⊦ (empty X) ∈ CC❙
  finite_union : {A,B} ⊦ A ∈ CC ⟶ ⊦ B ∈ CC ⟶ ⊦ A ∪ B ∈ CC❙
❚

theory NeighborhoodTopology =
  X     : tp❙
  NN    : tm X ⟶ tm ℘℘X❙
  neighborhood: tm X ⟶ tm ℘X ⟶ prop❘
              = [x,N] N ∈ (NN x)❘# 1 ∘ 2 prec 30❙
  
  nonempty : {x} ⊦ ¬ (NN x) ≐ ∅❙
  inneighborhood : {x: tm X,N} ⊦ x ∘ N ⟶ ⊦ x ∈ N❙
  superset_closed   : {M,N,x} ⊦ x ∘ M ⟶ ⊦ M ⊆ N ⟶ ⊦ x ∘ N❙
  intersection_closed : {M,N,x} ⊦ x ∘ M ⟶ ⊦ x ∘ N ⟶ ⊦ x ∘ M ∩ N❙
  openness       : {N,x} ⊦ x ∘ N ⟶ ⊦ ∃[M]∀[y] x ∘ M ∧ (y∈M ⇒ y∘N)❙
❚