Structure topologyTheory


Source File Identifier index Theory binding index

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


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14