Structure topologyTheory

signature topologyTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val closed_DEF : thm
    val closed_in : thm
    val hull : thm
    val istopology : thm
    val limpt : thm
    val neigh : thm
    val open_DEF : thm
    val subtopology : thm
    val topology_TY_DEF : thm
    val topology_tybij : thm
    val topspace : thm
  
  (*  Theorems  *)
    val BIGINTER_2 : thm
    val BIGUNION_2 : thm
    val CLOSED_IN_BIGINTER : thm
    val CLOSED_IN_BIGUNION : thm
    val CLOSED_IN_DIFF : thm
    val CLOSED_IN_EMPTY : thm
    val CLOSED_IN_IMP_SUBSET : thm
    val CLOSED_IN_INTER : thm
    val CLOSED_IN_OPEN_IN_COMPL : thm
    val CLOSED_IN_SUBSET : thm
    val CLOSED_IN_SUBTOPOLOGY : thm
    val CLOSED_IN_SUBTOPOLOGY_EMPTY : thm
    val CLOSED_IN_SUBTOPOLOGY_REFL : thm
    val CLOSED_IN_SUBTOPOLOGY_UNION : thm
    val CLOSED_IN_TOPSPACE : thm
    val CLOSED_IN_UNION : thm
    val CLOSED_LIMPT : thm
    val HULLS_EQ : thm
    val HULL_ANTIMONO : thm
    val HULL_EQ : thm
    val HULL_HULL : thm
    val HULL_IMAGE : thm
    val HULL_IMAGE_GALOIS : thm
    val HULL_IMAGE_SUBSET : thm
    val HULL_INC : thm
    val HULL_INDUCT : thm
    val HULL_MINIMAL : thm
    val HULL_MONO : thm
    val HULL_P : thm
    val HULL_P_AND_Q : thm
    val HULL_REDUNDANT : thm
    val HULL_REDUNDANT_EQ : thm
    val HULL_SUBSET : thm
    val HULL_UNION : thm
    val HULL_UNION_LEFT : thm
    val HULL_UNION_RIGHT : thm
    val HULL_UNION_SUBSET : thm
    val HULL_UNIQUE : thm
    val ISTOPOLOGY_OPEN_IN : thm
    val ISTOPOLOGY_SUBTOPOLOGY : thm
    val IS_HULL : thm
    val OPEN_IN_BIGINTER : thm
    val OPEN_IN_BIGUNION : thm
    val OPEN_IN_CLAUSES : thm
    val OPEN_IN_CLOSED_IN : thm
    val OPEN_IN_CLOSED_IN_EQ : thm
    val OPEN_IN_DIFF : thm
    val OPEN_IN_EMPTY : thm
    val OPEN_IN_IMP_SUBSET : thm
    val OPEN_IN_INTER : thm
    val OPEN_IN_SUBOPEN : thm
    val OPEN_IN_SUBSET : thm
    val OPEN_IN_SUBTOPOLOGY : thm
    val OPEN_IN_SUBTOPOLOGY_EMPTY : thm
    val OPEN_IN_SUBTOPOLOGY_REFL : thm
    val OPEN_IN_SUBTOPOLOGY_UNION : thm
    val OPEN_IN_TOPSPACE : thm
    val OPEN_IN_UNION : thm
    val OPEN_NEIGH : thm
    val OPEN_OWN_NEIGH : thm
    val OPEN_SUBOPEN : thm
    val OPEN_UNOPEN : thm
    val P_HULL : thm
    val SUBSET_HULL : thm
    val SUBTOPOLOGY_SUPERSET : thm
    val SUBTOPOLOGY_TOPSPACE : thm
    val SUBTOPOLOGY_UNIV : thm
    val TOPOLOGY_EQ : thm
    val TOPSPACE_SUBTOPOLOGY : thm
    val closed_topspace : thm
    val open_topspace : thm
  
  val topology_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [quotient] Parent theory of "topology"
   
   [closed_DEF]  Definition
      
      ⊢ ∀s. closed s ⇔ closed_in s 𝕌(:α)
   
   [closed_in]  Definition
      
      ⊢ ∀top s.
          closed_in top s ⇔
          s ⊆ topspace top ∧ open_in top (topspace top DIFF s)
   
   [hull]  Definition
      
      ⊢ ∀P s. P hull s = BIGINTER {t | P t ∧ s ⊆ t}
   
   [istopology]  Definition
      
      ⊢ ∀L. istopology L ⇔
            ∅ ∈ L ∧ (∀s t. s ∈ L ∧ t ∈ L ⇒ s ∩ t ∈ L) ∧
            ∀k. k ⊆ L ⇒ BIGUNION k ∈ L
   
   [limpt]  Definition
      
      ⊢ ∀top x S'.
          limpt top x S' ⇔ ∀N. neigh top (N,x) ⇒ ∃y. x ≠ y ∧ S' y ∧ N y
   
   [neigh]  Definition
      
      ⊢ ∀top N x. neigh top (N,x) ⇔ ∃P. open_in top P ∧ P ⊆ N ∧ P x
   
   [open_DEF]  Definition
      
      ⊢ ∀s. open s ⇔ open_in s 𝕌(:α)
   
   [subtopology]  Definition
      
      ⊢ ∀top u. subtopology top u = topology {s ∩ u | open_in top s}
   
   [topology_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION istopology rep
   
   [topology_tybij]  Definition
      
      ⊢ (∀a. topology (open_in a) = a) ∧
        ∀r. istopology r ⇔ open_in (topology r) = r
   
   [topspace]  Definition
      
      ⊢ ∀top. topspace top = BIGUNION {s | open_in top s}
   
   [BIGINTER_2]  Theorem
      
      ⊢ ∀s t. BIGINTER {s; t} = s ∩ t
   
   [BIGUNION_2]  Theorem
      
      ⊢ ∀s t. BIGUNION {s; t} = s ∪ t
   
   [CLOSED_IN_BIGINTER]  Theorem
      
      ⊢ ∀top k.
          k ≠ ∅ ∧ (∀s. s ∈ k ⇒ closed_in top s) ⇒
          closed_in top (BIGINTER k)
   
   [CLOSED_IN_BIGUNION]  Theorem
      
      ⊢ ∀top s.
          FINITE s ∧ (∀t. t ∈ s ⇒ closed_in top t) ⇒
          closed_in top (BIGUNION s)
   
   [CLOSED_IN_DIFF]  Theorem
      
      ⊢ ∀top s t.
          closed_in top s ∧ open_in top t ⇒ closed_in top (s DIFF t)
   
   [CLOSED_IN_EMPTY]  Theorem
      
      ⊢ ∀top. closed_in top ∅
   
   [CLOSED_IN_IMP_SUBSET]  Theorem
      
      ⊢ ∀top s t. closed_in (subtopology top s) t ⇒ t ⊆ s
   
   [CLOSED_IN_INTER]  Theorem
      
      ⊢ ∀top s t. closed_in top s ∧ closed_in top t ⇒ closed_in top (s ∩ t)
   
   [CLOSED_IN_OPEN_IN_COMPL]  Theorem
      
      ⊢ ∀top. closed top ⇒ ∀s. closed_in top s ⇔ open_in top (COMPL s)
   
   [CLOSED_IN_SUBSET]  Theorem
      
      ⊢ ∀top s. closed_in top s ⇒ s ⊆ topspace top
   
   [CLOSED_IN_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top u s.
          closed_in (subtopology top u) s ⇔ ∃t. closed_in top t ∧ s = t ∩ u
   
   [CLOSED_IN_SUBTOPOLOGY_EMPTY]  Theorem
      
      ⊢ ∀top s. closed_in (subtopology top ∅) s ⇔ s = ∅
   
   [CLOSED_IN_SUBTOPOLOGY_REFL]  Theorem
      
      ⊢ ∀top u. closed_in (subtopology top u) u ⇔ u ⊆ topspace top
   
   [CLOSED_IN_SUBTOPOLOGY_UNION]  Theorem
      
      ⊢ ∀top s t u.
          closed_in (subtopology top t) s ∧ closed_in (subtopology top u) s ⇒
          closed_in (subtopology top (t ∪ u)) s
   
   [CLOSED_IN_TOPSPACE]  Theorem
      
      ⊢ ∀top. closed_in top (topspace top)
   
   [CLOSED_IN_UNION]  Theorem
      
      ⊢ ∀top s t. closed_in top s ∧ closed_in top t ⇒ closed_in top (s ∪ t)
   
   [CLOSED_LIMPT]  Theorem
      
      ⊢ ∀top.
          closed top ⇒ ∀S'. closed_in top S' ⇔ ∀x. limpt top x S' ⇒ S' x
   
   [HULLS_EQ]  Theorem
      
      ⊢ ∀P s t.
          (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ∧ s ⊆ P hull t ∧
          t ⊆ P hull s ⇒
          P hull s = P hull t
   
   [HULL_ANTIMONO]  Theorem
      
      ⊢ ∀P Q s. P ⊆ Q ⇒ Q hull s ⊆ P hull s
   
   [HULL_EQ]  Theorem
      
      ⊢ ∀P s.
          (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ (P hull s = s ⇔ P s)
   
   [HULL_HULL]  Theorem
      
      ⊢ ∀P s. P hull (P hull s) = P hull s
   
   [HULL_IMAGE]  Theorem
      
      ⊢ ∀P f s.
          (∀s. P (P hull s)) ∧ (∀s. P (IMAGE f s) ⇔ P s) ∧
          (∀x y. f x = f y ⇒ x = y) ∧ (∀y. ∃x. f x = y) ⇒
          P hull IMAGE f s = IMAGE f (P hull s)
   
   [HULL_IMAGE_GALOIS]  Theorem
      
      ⊢ ∀P f g s.
          (∀s. P (P hull s)) ∧ (∀s. P s ⇒ P (IMAGE f s)) ∧
          (∀s. P s ⇒ P (IMAGE g s)) ∧ (∀s t. s ⊆ IMAGE g t ⇔ IMAGE f s ⊆ t) ⇒
          P hull IMAGE f s = IMAGE f (P hull s)
   
   [HULL_IMAGE_SUBSET]  Theorem
      
      ⊢ ∀P f s.
          P (P hull s) ∧ (∀s. P s ⇒ P (IMAGE f s)) ⇒
          P hull IMAGE f s ⊆ IMAGE f (P hull s)
   
   [HULL_INC]  Theorem
      
      ⊢ ∀P s x. x ∈ s ⇒ x ∈ P hull s
   
   [HULL_INDUCT]  Theorem
      
      ⊢ ∀P p s. (∀x. x ∈ s ⇒ p x) ∧ P {x | p x} ⇒ ∀x. x ∈ P hull s ⇒ p x
   
   [HULL_MINIMAL]  Theorem
      
      ⊢ ∀P s t. s ⊆ t ∧ P t ⇒ P hull s ⊆ t
   
   [HULL_MONO]  Theorem
      
      ⊢ ∀P s t. s ⊆ t ⇒ P hull s ⊆ P hull t
   
   [HULL_P]  Theorem
      
      ⊢ ∀P s. P s ⇒ P hull s = s
   
   [HULL_P_AND_Q]  Theorem
      
      ⊢ ∀P Q.
          (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ∧
          (∀f. (∀s. s ∈ f ⇒ Q s) ⇒ Q (BIGINTER f)) ∧
          (∀s. Q s ⇒ Q (P hull s)) ⇒
          (λx. P x ∧ Q x) hull s = P hull (Q hull s)
   
   [HULL_REDUNDANT]  Theorem
      
      ⊢ ∀P a s. a ∈ P hull s ⇒ P hull (a INSERT s) = P hull s
   
   [HULL_REDUNDANT_EQ]  Theorem
      
      ⊢ ∀P a s. a ∈ P hull s ⇔ P hull (a INSERT s) = P hull s
   
   [HULL_SUBSET]  Theorem
      
      ⊢ ∀P s. s ⊆ P hull s
   
   [HULL_UNION]  Theorem
      
      ⊢ ∀P s t. P hull s ∪ t = P hull (P hull s) ∪ (P hull t)
   
   [HULL_UNION_LEFT]  Theorem
      
      ⊢ ∀P s t. P hull s ∪ t = P hull (P hull s) ∪ t
   
   [HULL_UNION_RIGHT]  Theorem
      
      ⊢ ∀P s t. P hull s ∪ t = P hull s ∪ (P hull t)
   
   [HULL_UNION_SUBSET]  Theorem
      
      ⊢ ∀P s t. (P hull s) ∪ (P hull t) ⊆ P hull s ∪ t
   
   [HULL_UNIQUE]  Theorem
      
      ⊢ ∀P s t. s ⊆ t ∧ P t ∧ (∀t'. s ⊆ t' ∧ P t' ⇒ t ⊆ t') ⇒ P hull s = t
   
   [ISTOPOLOGY_OPEN_IN]  Theorem
      
      ⊢ ∀top. istopology (open_in top)
   
   [ISTOPOLOGY_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top u. istopology {s ∩ u | open_in top s}
   
   [IS_HULL]  Theorem
      
      ⊢ ∀P s.
          (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒
          (P s ⇔ ∃t. s = P hull t)
   
   [OPEN_IN_BIGINTER]  Theorem
      
      ⊢ ∀top s.
          FINITE s ∧ s ≠ ∅ ∧ (∀t. t ∈ s ⇒ open_in top t) ⇒
          open_in top (BIGINTER s)
   
   [OPEN_IN_BIGUNION]  Theorem
      
      ⊢ ∀top k. (∀s. s ∈ k ⇒ open_in top s) ⇒ open_in top (BIGUNION k)
   
   [OPEN_IN_CLAUSES]  Theorem
      
      ⊢ ∀top.
          open_in top ∅ ∧
          (∀s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∩ t)) ∧
          ∀k. (∀s. s ∈ k ⇒ open_in top s) ⇒ open_in top (BIGUNION k)
   
   [OPEN_IN_CLOSED_IN]  Theorem
      
      ⊢ ∀top s.
          s ⊆ topspace top ⇒
          (open_in top s ⇔ closed_in top (topspace top DIFF s))
   
   [OPEN_IN_CLOSED_IN_EQ]  Theorem
      
      ⊢ ∀top s.
          open_in top s ⇔
          s ⊆ topspace top ∧ closed_in top (topspace top DIFF s)
   
   [OPEN_IN_DIFF]  Theorem
      
      ⊢ ∀top s t. open_in top s ∧ closed_in top t ⇒ open_in top (s DIFF t)
   
   [OPEN_IN_EMPTY]  Theorem
      
      ⊢ ∀top. open_in top ∅
   
   [OPEN_IN_IMP_SUBSET]  Theorem
      
      ⊢ ∀top s t. open_in (subtopology top s) t ⇒ t ⊆ s
   
   [OPEN_IN_INTER]  Theorem
      
      ⊢ ∀top s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∩ t)
   
   [OPEN_IN_SUBOPEN]  Theorem
      
      ⊢ ∀top s.
          open_in top s ⇔ ∀x. x ∈ s ⇒ ∃t. open_in top t ∧ x ∈ t ∧ t ⊆ s
   
   [OPEN_IN_SUBSET]  Theorem
      
      ⊢ ∀top s. open_in top s ⇒ s ⊆ topspace top
   
   [OPEN_IN_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top u s.
          open_in (subtopology top u) s ⇔ ∃t. open_in top t ∧ s = t ∩ u
   
   [OPEN_IN_SUBTOPOLOGY_EMPTY]  Theorem
      
      ⊢ ∀top s. open_in (subtopology top ∅) s ⇔ s = ∅
   
   [OPEN_IN_SUBTOPOLOGY_REFL]  Theorem
      
      ⊢ ∀top u. open_in (subtopology top u) u ⇔ u ⊆ topspace top
   
   [OPEN_IN_SUBTOPOLOGY_UNION]  Theorem
      
      ⊢ ∀top s t u.
          open_in (subtopology top t) s ∧ open_in (subtopology top u) s ⇒
          open_in (subtopology top (t ∪ u)) s
   
   [OPEN_IN_TOPSPACE]  Theorem
      
      ⊢ ∀top. open_in top (topspace top)
   
   [OPEN_IN_UNION]  Theorem
      
      ⊢ ∀top s t. open_in top s ∧ open_in top t ⇒ open_in top (s ∪ t)
   
   [OPEN_NEIGH]  Theorem
      
      ⊢ ∀S' top. open_in top S' ⇔ ∀x. S' x ⇒ ∃N. neigh top (N,x) ∧ N ⊆ S'
   
   [OPEN_OWN_NEIGH]  Theorem
      
      ⊢ ∀S' top x. open_in top S' ∧ S' x ⇒ neigh top (S',x)
   
   [OPEN_SUBOPEN]  Theorem
      
      ⊢ ∀S' top.
          open_in top S' ⇔ ∀x. S' x ⇒ ∃P. P x ∧ open_in top P ∧ P ⊆ S'
   
   [OPEN_UNOPEN]  Theorem
      
      ⊢ ∀S' top.
          open_in top S' ⇔ BIGUNION {P | open_in top P ∧ P ⊆ S'} = S'
   
   [P_HULL]  Theorem
      
      ⊢ ∀P s. (∀f. (∀s. s ∈ f ⇒ P s) ⇒ P (BIGINTER f)) ⇒ P (P hull s)
   
   [SUBSET_HULL]  Theorem
      
      ⊢ ∀P s t. P t ⇒ (P hull s ⊆ t ⇔ s ⊆ t)
   
   [SUBTOPOLOGY_SUPERSET]  Theorem
      
      ⊢ ∀top s. topspace top ⊆ s ⇒ subtopology top s = top
   
   [SUBTOPOLOGY_TOPSPACE]  Theorem
      
      ⊢ ∀top. subtopology top (topspace top) = top
   
   [SUBTOPOLOGY_UNIV]  Theorem
      
      ⊢ ∀top. subtopology top 𝕌(:α) = top
   
   [TOPOLOGY_EQ]  Theorem
      
      ⊢ ∀top1 top2. top1 = top2 ⇔ ∀s. open_in top1 s ⇔ open_in top2 s
   
   [TOPSPACE_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top u. topspace (subtopology top u) = topspace top ∩ u
   
   [closed_topspace]  Theorem
      
      ⊢ ∀top. closed top ⇒ topspace top = 𝕌(:α)
   
   [open_topspace]  Theorem
      
      ⊢ ∀top. open top ⇒ topspace top = 𝕌(:α)
   
   
*)
end

HOL 4, Kananaskis-14