:: OPENLATT semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v1_lattice2 :::"Heyting"::: ) -> ($#v3_filter_0 :::"implicative"::: ) for ($#l3_lattices :::"LattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v3_filter_0 :::"implicative"::: ) -> ($#v14_lattices :::"upper-bounded"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: OPENLATT:1 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: OPENLATT:2 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ))))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; func :::"Topology_of"::: "T" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: OPENLATT:def 1 (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T"); end; :: deftheorem defines :::"Topology_of"::: OPENLATT:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))))); registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k1_openlatt :::"Topology_of"::: ) "T") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "P", "Q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) (Set (Const "T"))); :: original: :::"\/"::: redefine func "P" :::"\/"::: "Q" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) "T"); :: original: :::"/\"::: redefine func "P" :::"/\"::: "Q" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) "T"); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"Top_Union"::: "T" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) "T" ")" ) means :: OPENLATT:def 2 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) "T") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k2_openlatt :::"\/"::: ) (Set (Var "Q"))))); func :::"Top_Meet"::: "T" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) "T" ")" ) means :: OPENLATT:def 3 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) "T") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_openlatt :::"/\"::: ) (Set (Var "Q"))))); end; :: deftheorem defines :::"Top_Union"::: OPENLATT:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_openlatt :::"Top_Union"::: ) (Set (Var "T")))) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k2_openlatt :::"\/"::: ) (Set (Var "Q"))))) ")" ))); :: deftheorem defines :::"Top_Meet"::: OPENLATT:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_openlatt :::"Top_Meet"::: ) (Set (Var "T")))) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_openlatt :::"/\"::: ) (Set (Var "Q"))))) ")" ))); theorem :: OPENLATT:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k4_openlatt :::"Top_Union"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k5_openlatt :::"Top_Meet"::: ) (Set (Var "T")) ")" ) "#)" ) "is" ($#l3_lattices :::"Lattice":::))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"Open_setLatt"::: "T" -> ($#l3_lattices :::"Lattice":::) equals :: OPENLATT:def 4 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) "T" ")" ) "," (Set "(" ($#k4_openlatt :::"Top_Union"::: ) "T" ")" ) "," (Set "(" ($#k5_openlatt :::"Top_Meet"::: ) "T" ")" ) "#)" ); end; :: deftheorem defines :::"Open_setLatt"::: OPENLATT:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k4_openlatt :::"Top_Union"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k5_openlatt :::"Top_Meet"::: ) (Set (Var "T")) ")" ) "#)" ))); theorem :: OPENLATT:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T"))))) ; theorem :: OPENLATT:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "q")))) ")" ))) ; theorem :: OPENLATT:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "q"))) ")" ))) ; theorem :: OPENLATT:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T")) ")" ) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_openlatt :::"Topology_of"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "p9")) ($#r1_tarski :::"c="::: ) (Set (Var "q9"))) ")" )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k6_openlatt :::"Open_setLatt"::: ) "T") -> ($#v3_filter_0 :::"implicative"::: ) ; end; theorem :: OPENLATT:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T"))) "is" ($#v13_lattices :::"lower-bounded"::: ) ) & (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k6_openlatt :::"Open_setLatt"::: ) "T") -> ($#v1_lattice2 :::"Heyting"::: ) ; end; theorem :: OPENLATT:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) ; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); func :::"F_primeSet"::: "L" -> ($#m1_hidden :::"set"::: ) equals :: OPENLATT:def 5 "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Filter":::) "of" "L" : (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set (Var "F")) "is" ($#v2_filter_0 :::"prime"::: ) ) ")" ) "}" ; end; :: deftheorem defines :::"F_primeSet"::: OPENLATT:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) "holds" (Bool (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "F")) "is" ($#v2_filter_0 :::"prime"::: ) ) ")" ) "}" )); theorem :: OPENLATT:10 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "L")))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "F")) "is" ($#v2_filter_0 :::"prime"::: ) ) ")" ) ")" ))) ; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); func :::"StoneH"::: "L" -> ($#m1_hidden :::"Function":::) means :: OPENLATT:def 6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Filter":::) "of" "L" : (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) "L")) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" ) ")" )); end; :: deftheorem defines :::"StoneH"::: OPENLATT:def 6 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "L")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" ) ")" )) ")" ))); theorem :: OPENLATT:11 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "L")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) ")" )))) ; theorem :: OPENLATT:12 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "F")) "is" ($#v2_filter_0 :::"prime"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" )))) ; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); func :::"StoneS"::: "L" -> ($#m1_hidden :::"set"::: ) equals :: OPENLATT:def 7 (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k8_openlatt :::"StoneH"::: ) "L" ")" )); end; :: deftheorem defines :::"StoneS"::: OPENLATT:def 7 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) "holds" (Bool (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" )))); registrationlet "L" be ($#l3_lattices :::"D_Lattice":::); cluster (Set ($#k9_openlatt :::"StoneS"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: OPENLATT:13 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" ))) ; theorem :: OPENLATT:14 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))))) ; theorem :: OPENLATT:15 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))))) ; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"SF_have"::: "a" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "L" equals :: OPENLATT:def 8 "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Filter":::) "of" "L" : (Bool "a" ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ; end; :: deftheorem defines :::"SF_have"::: OPENLATT:def 8 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k10_openlatt :::"SF_have"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))); registrationlet "L" be ($#l3_lattices :::"D_Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k10_openlatt :::"SF_have"::: ) "a") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: OPENLATT:16 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_openlatt :::"SF_have"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" ) ")" )))) ; theorem :: OPENLATT:17 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "b")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "a")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) ")" )))) ; theorem :: OPENLATT:18 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "b")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "Z")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "b")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "a")) ")" ))) & (Bool "(" "for" (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ))))) ; theorem :: OPENLATT:19 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Bool "not" (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k2_filter_0 :::"<."::: ) (Set (Var "b")) ($#k2_filter_0 :::".)"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "b")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_openlatt :::"SF_have"::: ) (Set (Var "a")) ")" ))))) ; theorem :: OPENLATT:20 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Bool "not" (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "a"))))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )))) ; theorem :: OPENLATT:21 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "L"))))))) ; theorem :: OPENLATT:22 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k8_openlatt :::"StoneH"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))) ; registrationlet "L" be ($#l3_lattices :::"D_Lattice":::); cluster (Set ($#k8_openlatt :::"StoneH"::: ) "L") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); let "A", "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Const "L"))); :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) "L"); :: original: :::"/\"::: redefine func "A" :::"/\"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) "L"); end; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); func :::"Set_Union"::: "L" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) "L" ")" ) means :: OPENLATT:def 9 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) "L") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k11_openlatt :::"\/"::: ) (Set (Var "B"))))); func :::"Set_Meet"::: "L" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) "L" ")" ) means :: OPENLATT:def 10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) "L") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k12_openlatt :::"/\"::: ) (Set (Var "B"))))); end; :: deftheorem defines :::"Set_Union"::: OPENLATT:def 9 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_openlatt :::"Set_Union"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k11_openlatt :::"\/"::: ) (Set (Var "B"))))) ")" ))); :: deftheorem defines :::"Set_Meet"::: OPENLATT:def 10 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_openlatt :::"Set_Meet"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k12_openlatt :::"/\"::: ) (Set (Var "B"))))) ")" ))); theorem :: OPENLATT:23 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k13_openlatt :::"Set_Union"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k14_openlatt :::"Set_Meet"::: ) (Set (Var "L")) ")" ) "#)" ) "is" ($#l3_lattices :::"Lattice":::))) ; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); func :::"StoneLatt"::: "L" -> ($#l3_lattices :::"Lattice":::) equals :: OPENLATT:def 11 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k9_openlatt :::"StoneS"::: ) "L" ")" ) "," (Set "(" ($#k13_openlatt :::"Set_Union"::: ) "L" ")" ) "," (Set "(" ($#k14_openlatt :::"Set_Meet"::: ) "L" ")" ) "#)" ); end; :: deftheorem defines :::"StoneLatt"::: OPENLATT:def 11 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) "holds" (Bool (Set ($#k15_openlatt :::"StoneLatt"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k13_openlatt :::"Set_Union"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k14_openlatt :::"Set_Meet"::: ) (Set (Var "L")) ")" ) "#)" ))); theorem :: OPENLATT:24 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_openlatt :::"StoneLatt"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "L"))))) ; theorem :: OPENLATT:25 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_openlatt :::"StoneLatt"::: ) (Set (Var "L")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "q")))) ")" ))) ; theorem :: OPENLATT:26 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_openlatt :::"StoneLatt"::: ) (Set (Var "L")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "q"))) ")" ))) ; definitionlet "L" be ($#l3_lattices :::"D_Lattice":::); :: original: :::"StoneH"::: redefine func :::"StoneH"::: "L" -> ($#m1_lattice4 :::"Homomorphism"::: ) "of" "L" "," (Set ($#k15_openlatt :::"StoneLatt"::: ) "L"); end; registrationlet "L" be ($#l3_lattices :::"D_Lattice":::); cluster (Set ($#k8_openlatt :::"StoneH"::: ) "L") -> ($#v3_funct_2 :::"bijective"::: ) for ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k15_openlatt :::"StoneLatt"::: ) "L" ")" ); cluster (Set ($#k15_openlatt :::"StoneLatt"::: ) "L") -> ($#v11_lattices :::"distributive"::: ) ; end; theorem :: OPENLATT:27 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) "holds" (Bool (Set (Var "L")) "," (Set ($#k15_openlatt :::"StoneLatt"::: ) (Set (Var "L"))) ($#r1_filter_1 :::"are_isomorphic"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v11_lattices :::"distributive"::: ) ($#v12_lattices :::"modular"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) bbbadV15_LATTICES() ($#v1_lattice2 :::"Heyting"::: ) ($#v3_filter_0 :::"implicative"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: OPENLATT:28 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set (Set "(" ($#k16_openlatt :::"StoneH"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "H"))))) ; theorem :: OPENLATT:29 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set (Set "(" ($#k16_openlatt :::"StoneH"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: OPENLATT:30 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "H")) ")" )))) ; registrationlet "H" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::); cluster (Set ($#k7_openlatt :::"F_primeSet"::: ) "H") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "H" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::); func :::"HTopSpace"::: "H" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) means :: OPENLATT:def 12 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) "H")) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) "H" ")" ) : (Bool verum) "}" ) ")" ); end; :: deftheorem defines :::"HTopSpace"::: OPENLATT:def 12 : (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k17_openlatt :::"HTopSpace"::: ) (Set (Var "H")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_openlatt :::"F_primeSet"::: ) (Set (Var "H")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) (Set (Var "H")) ")" ) : (Bool verum) "}" ) ")" ) ")" ))); registrationlet "H" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::); cluster (Set ($#k17_openlatt :::"HTopSpace"::: ) "H") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; theorem :: OPENLATT:31 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set "(" ($#k17_openlatt :::"HTopSpace"::: ) (Set (Var "H")) ")" ) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_openlatt :::"StoneS"::: ) (Set (Var "H")) ")" ) : (Bool verum) "}" )) ; theorem :: OPENLATT:32 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set ($#k9_openlatt :::"StoneS"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_openlatt :::"Open_setLatt"::: ) (Set "(" ($#k17_openlatt :::"HTopSpace"::: ) (Set (Var "H")) ")" ) ")" )))) ; definitionlet "H" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::); :: original: :::"StoneH"::: redefine func :::"StoneH"::: "H" -> ($#m1_lattice4 :::"Homomorphism"::: ) "of" "H" "," (Set ($#k6_openlatt :::"Open_setLatt"::: ) (Set "(" ($#k17_openlatt :::"HTopSpace"::: ) "H" ")" )); end; theorem :: OPENLATT:33 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set "(" ($#k18_openlatt :::"StoneH"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p9")) ($#k4_filter_0 :::"=>"::: ) (Set (Var "q9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_openlatt :::"StoneH"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p9")) ")" ) ($#k4_filter_0 :::"=>"::: ) (Set "(" (Set "(" ($#k18_openlatt :::"StoneH"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q9")) ")" ))))) ; theorem :: OPENLATT:34 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set ($#k18_openlatt :::"StoneH"::: ) (Set (Var "H"))) ($#r1_lattice4 :::"preserves_implication"::: ) )) ; theorem :: OPENLATT:35 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set ($#k18_openlatt :::"StoneH"::: ) (Set (Var "H"))) ($#r2_lattice4 :::"preserves_top"::: ) )) ; theorem :: OPENLATT:36 (Bool "for" (Set (Var "H")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l3_lattices :::"H_Lattice":::) "holds" (Bool (Set ($#k18_openlatt :::"StoneH"::: ) (Set (Var "H"))) ($#r3_lattice4 :::"preserves_bottom"::: ) )) ;