:: TOPGRP_1 semantic presentation begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) bbbadV1_PARTFUN1("X") ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_funct_2 :::"onto"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: TOPGRP_1:1 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S"))))) ; registrationlet "R" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set (Set "(" ($#k3_struct_0 :::"id"::: ) "R" ")" ) ($#k2_tops_2 :::"/""::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: TOPGRP_1:2 (Bool "for" (Set (Var "R")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "R")) ")" ) ($#k2_tops_2 :::"/""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "R"))))) ; theorem :: TOPGRP_1:3 (Bool "for" (Set (Var "R")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "R")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; begin theorem :: TOPGRP_1:4 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "," (Set (Var "Q")) "," (Set (Var "Q1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "Q1")))) "holds" (Bool (Set (Set (Var "P")) ($#k2_group_2 :::"*"::: ) (Set (Var "Q"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P1")) ($#k2_group_2 :::"*"::: ) (Set (Var "Q1")))))) ; theorem :: TOPGRP_1:5 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "H")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set (Var "P")) ($#k5_group_2 :::"*"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Q")) ($#k5_group_2 :::"*"::: ) (Set (Var "h"))))))) ; theorem :: TOPGRP_1:6 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "H")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set (Var "h")) ($#k4_group_2 :::"*"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "h")) ($#k4_group_2 :::"*"::: ) (Set (Var "Q"))))))) ; theorem :: TOPGRP_1:7 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) )) "iff" (Bool (Set (Set (Var "a")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )))) ; theorem :: TOPGRP_1:8 canceled; theorem :: TOPGRP_1:9 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_group_2 :::"""::: ) )) ")" ))) ; theorem :: TOPGRP_1:10 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) )))) ; theorem :: TOPGRP_1:11 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) )))) ; theorem :: TOPGRP_1:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; theorem :: TOPGRP_1:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k3_group_1 :::"inverse_op"::: ) "G") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; theorem :: TOPGRP_1:14 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G")) ")" ) ($#k2_funct_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G"))))) ; theorem :: TOPGRP_1:15 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k2_group_2 :::"*"::: ) (Set (Var "Q")))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "a" :::"*"::: -> ($#m1_subset_1 :::"Function":::) "of" "G" "," "G" means :: TOPGRP_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))); func :::"*"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" "G" "," "G" means :: TOPGRP_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) "a"))); end; :: deftheorem defines :::"*"::: TOPGRP_1:def 1 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_topgrp_1 :::"*"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))) ")" )))); :: deftheorem defines :::"*"::: TOPGRP_1:def 2 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_topgrp_1 :::"*"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) ")" )))); registrationlet "G" be ($#l3_algstr_0 :::"Group":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "a" ($#k1_topgrp_1 :::"*"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; cluster (Set ($#k2_topgrp_1 :::"*"::: ) "a") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; theorem :: TOPGRP_1:16 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "H")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_topgrp_1 :::"*"::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k4_group_2 :::"*"::: ) (Set (Var "P"))))))) ; theorem :: TOPGRP_1:17 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "H")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set "(" ($#k2_topgrp_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k5_group_2 :::"*"::: ) (Set (Var "h"))))))) ; theorem :: TOPGRP_1:18 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_topgrp_1 :::"*"::: ) ")" ) ($#k2_tops_2 :::"/""::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k1_topgrp_1 :::"*"::: ) )))) ; theorem :: TOPGRP_1:19 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k2_topgrp_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_tops_2 :::"/""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k2_topgrp_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ))))) ; begin registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set (Set "(" ($#k3_struct_0 :::"id"::: ) "T" ")" ) ($#k2_tops_2 :::"/""::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPGRP_1:20 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" "p"; end; theorem :: TOPGRP_1:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p"))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_pre_topc :::"open"::: ) for ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" "p"; end; theorem :: TOPGRP_1:22 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_t_0topsp :::"open"::: ) )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) (Bool "ex" (Set (Var "R")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) "st" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))))))) ; theorem :: TOPGRP_1:23 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) (Bool "ex" (Set (Var "R")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) "st" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")))))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v1_t_0topsp :::"open"::: ) ))) ; theorem :: TOPGRP_1:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) ")" ) ")" ) ")" ))) ; theorem :: TOPGRP_1:25 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ) ")" ) ")" ) ")" ))) ; theorem :: TOPGRP_1:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ) ")" ) ")" ) ")" ))) ; theorem :: TOPGRP_1:27 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "P")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P")) ")" )))) ")" )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_tops_1 :::"dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: TOPGRP_1:28 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v1_tops_1 :::"dense"::: ) )))) ; theorem :: TOPGRP_1:29 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) "is" ($#v1_tops_1 :::"dense"::: ) )))) ; registrationlet "S", "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_tops_2 :::"being_homeomorphism"::: ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_tops_2 :::"being_homeomorphism"::: ) -> ($#v1_t_0topsp :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_tops_2 :::"being_homeomorphism"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#v3_tops_2 :::"being_homeomorphism"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "T")); cluster (Set "f" ($#k2_tops_2 :::"/""::: ) ) -> ($#v3_tops_2 :::"being_homeomorphism"::: ) ; end; begin definitionlet "S", "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; assume (Bool (Set (Const "S")) "," (Set (Const "T")) ($#r1_t_0topsp :::"are_homeomorphic"::: ) ) ; mode :::"Homeomorphism"::: "of" "S" "," "T" -> ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" means :: TOPGRP_1:def 3 (Bool it "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ); end; :: deftheorem defines :::"Homeomorphism"::: TOPGRP_1:def 3 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r1_t_0topsp :::"are_homeomorphic"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))) "iff" (Bool (Set (Var "b3")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; mode :::"Homeomorphism"::: "of" "T" -> ($#m1_subset_1 :::"Function":::) "of" "T" "," "T" means :: TOPGRP_1:def 4 (Bool it "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ); end; :: deftheorem defines :::"Homeomorphism"::: TOPGRP_1:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "b2")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; :: original: :::"Homeomorphism"::: redefine mode :::"Homeomorphism"::: "of" "T" -> ($#m1_topgrp_1 :::"Homeomorphism"::: ) "of" "T" "," "T"; end; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; :: original: :::"id"::: redefine func :::"id"::: "T" -> ($#m1_topgrp_1 :::"Homeomorphism"::: ) "of" "T" "," "T"; end; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; :: original: :::"id"::: redefine func :::"id"::: "T" -> ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "T"; end; registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster -> ($#v3_tops_2 :::"being_homeomorphism"::: ) for ($#m2_topgrp_1 :::"Homeomorphism"::: ) "of" "T"; end; theorem :: TOPGRP_1:30 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"/""::: ) ) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T"))))) ; theorem :: TOPGRP_1:31 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T"))))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; func :::"HomeoGroup"::: "T" -> ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: TOPGRP_1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) "implies" (Bool (Set (Var "x")) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "T") ")" & "(" (Bool (Bool (Set (Var "x")) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "T")) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) ")" & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "T" "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) ")" ) ")" )); end; :: deftheorem defines :::"HomeoGroup"::: TOPGRP_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_topgrp_1 :::"HomeoGroup"::: ) (Set (Var "T")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) "implies" (Bool (Set (Var "x")) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "x")) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) ")" & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) ")" ) ")" )) ")" ))); registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k5_topgrp_1 :::"HomeoGroup"::: ) "T") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: TOPGRP_1:32 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_topgrp_1 :::"HomeoGroup"::: ) (Set (Var "T")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k5_topgrp_1 :::"HomeoGroup"::: ) "T") -> ($#v15_algstr_0 :::"strict"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ; end; theorem :: TOPGRP_1:33 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k4_topgrp_1 :::"id"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k5_topgrp_1 :::"HomeoGroup"::: ) (Set (Var "T")) ")" )))) ; theorem :: TOPGRP_1:34 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_topgrp_1 :::"HomeoGroup"::: ) (Set (Var "T")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_tops_2 :::"/""::: ) ))))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"homogeneous"::: means :: TOPGRP_1:def 6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" (Bool "ex" (Set (Var "f")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "T" "st" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))))); end; :: deftheorem defines :::"homogeneous"::: TOPGRP_1:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_topgrp_1 :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "f")) "being" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "T")) "st" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))))) ")" )); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_topgrp_1 :::"homogeneous"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TOPGRP_1:35 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topgrp_1 :::"homogeneous"::: ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ))) "holds" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) ; theorem :: TOPGRP_1:36 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topgrp_1 :::"homogeneous"::: ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))))) "holds" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) )) ; begin definitionattr "c1" is :::"strict"::: ; struct :::"TopGrStr"::: -> ($#l3_algstr_0 :::"multMagma"::: ) "," ($#l1_pre_topc :::"TopStruct"::: ) ; aggr :::"TopGrStr":::(# :::"carrier":::, :::"multF":::, :::"topology"::: #) -> ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "T" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "A")); cluster (Set ($#g1_topgrp_1 :::"TopGrStr"::: ) "(#" "A" "," "R" "," "T" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Const "x")) ($#k1_tarski :::"}"::: ) ); let "T" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Const "x")) ($#k1_tarski :::"}"::: ) ); cluster (Set ($#g1_topgrp_1 :::"TopGrStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," "R" "," "T" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_compts_1 :::"1TopSp"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) )) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topgrp_1 :::"strict"::: ) for ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_topgrp_1 :::"strict"::: ) for ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) ; attr "G" is :::"UnContinuous"::: means :: TOPGRP_1:def 7 (Bool (Set ($#k3_group_1 :::"inverse_op"::: ) "G") "is" ($#v5_pre_topc :::"continuous"::: ) ); end; :: deftheorem defines :::"UnContinuous"::: TOPGRP_1:def 7 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_topgrp_1 :::"UnContinuous"::: ) ) "iff" (Bool (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G"))) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )); definitionlet "G" be ($#v2_pre_topc :::"TopSpace-like"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) ; attr "G" is :::"BinContinuous"::: means :: TOPGRP_1:def 8 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) "G" "," "G" ($#k2_borsuk_1 :::":]"::: ) ) "," "G" "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G"))) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )); end; :: deftheorem defines :::"BinContinuous"::: TOPGRP_1:def 8 : (Bool "for" (Set (Var "G")) "being" ($#v2_pre_topc :::"TopSpace-like"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v4_topgrp_1 :::"BinContinuous"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "G")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "G")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))))) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) bbbadV8_STRUCT_0() (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_compts_1 :::"compact"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_topgrp_1 :::"homogeneous"::: ) ($#v2_topgrp_1 :::"strict"::: ) ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#v4_topgrp_1 :::"BinContinuous"::: ) for ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; definitionmode TopGroup is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; definitionmode TopologicalGroup is ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); end; theorem :: TOPGRP_1:37 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) (Bool "ex" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a"))(Bool "ex" (Set (Var "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "b")) "st" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "W")))))))) ; theorem :: TOPGRP_1:38 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) (Bool "ex" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a"))(Bool "ex" (Set (Var "B")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "b")) "st" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "W")))))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v4_topgrp_1 :::"BinContinuous"::: ) )) ; theorem :: TOPGRP_1:39 (Bool "for" (Set (Var "T")) "being" ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k2_group_1 :::"""::: ) ) (Bool "ex" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a")) "st" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "W"))))))) ; theorem :: TOPGRP_1:40 (Bool "for" (Set (Var "T")) "being" ($#l1_topgrp_1 :::"TopGroup":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k2_group_1 :::"""::: ) ) (Bool "ex" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a")) "st" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "W"))))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v3_topgrp_1 :::"UnContinuous"::: ) )) ; theorem :: TOPGRP_1:41 (Bool "for" (Set (Var "T")) "being" ($#l1_topgrp_1 :::"TopologicalGroup":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" )) (Bool "ex" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a"))(Bool "ex" (Set (Var "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "b")) "st" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k1_group_2 :::"""::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "W")))))))) ; theorem :: TOPGRP_1:42 (Bool "for" (Set (Var "T")) "being" ($#l1_topgrp_1 :::"TopGroup":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "W")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" )) (Bool "ex" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a"))(Bool "ex" (Set (Var "B")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "b")) "st" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k1_group_2 :::"""::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "W")))))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#l1_topgrp_1 :::"TopologicalGroup":::))) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGrStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "a" ($#k1_topgrp_1 :::"*"::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; cluster (Set ($#k2_topgrp_1 :::"*"::: ) "a") -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPGRP_1:43 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k1_topgrp_1 :::"*"::: ) ) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "G"))))) ; theorem :: TOPGRP_1:44 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_topgrp_1 :::"*"::: ) (Set (Var "a"))) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "G"))))) ; definitionlet "G" be ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); :: original: :::"*"::: redefine func "a" :::"*"::: -> ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "G"; :: original: :::"*"::: redefine func :::"*"::: "a" -> ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "G"; end; theorem :: TOPGRP_1:45 (Bool "for" (Set (Var "G")) "being" ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) "holds" (Bool (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G"))) "is" ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" (Set (Var "G")))) ; definitionlet "G" be ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); :: original: :::"inverse_op"::: redefine func :::"inverse_op"::: "G" -> ($#m3_topgrp_1 :::"Homeomorphism"::: ) "of" "G"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_topgrp_1 :::"BinContinuous"::: ) -> ($#v1_topgrp_1 :::"homogeneous"::: ) for ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; theorem :: TOPGRP_1:46 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "F")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "F")) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) "is" ($#v4_pre_topc :::"closed"::: ) )))) ; theorem :: TOPGRP_1:47 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "F")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set (Var "F"))) "is" ($#v4_pre_topc :::"closed"::: ) )))) ; registrationlet "G" be ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "F" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "F" ($#k5_group_2 :::"*"::: ) "a") -> ($#v4_pre_topc :::"closed"::: ) ; cluster (Set "a" ($#k4_group_2 :::"*"::: ) "F") -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: TOPGRP_1:48 (Bool "for" (Set (Var "G")) "being" ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "F")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "F")) ($#k1_group_2 :::"""::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; registrationlet "G" be ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "F" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); cluster (Set "F" ($#k1_group_2 :::"""::: ) ) -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: TOPGRP_1:49 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "O")) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: TOPGRP_1:50 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set (Var "O"))) "is" ($#v3_pre_topc :::"open"::: ) )))) ; registrationlet "G" be ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "A" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "A" ($#k5_group_2 :::"*"::: ) "a") -> ($#v3_pre_topc :::"open"::: ) ; cluster (Set "a" ($#k4_group_2 :::"*"::: ) "A") -> ($#v3_pre_topc :::"open"::: ) ; end; theorem :: TOPGRP_1:51 (Bool "for" (Set (Var "G")) "being" ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "O")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "O")) ($#k1_group_2 :::"""::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ))) ; registrationlet "G" be ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "A" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); cluster (Set "A" ($#k1_group_2 :::"""::: ) ) -> ($#v3_pre_topc :::"open"::: ) ; end; theorem :: TOPGRP_1:52 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "A")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "O")) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPGRP_1:53 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "A")) "," (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "O"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; registrationlet "G" be ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "A" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); cluster (Set "A" ($#k2_group_2 :::"*"::: ) "B") -> ($#v3_pre_topc :::"open"::: ) ; cluster (Set "B" ($#k2_group_2 :::"*"::: ) "A") -> ($#v3_pre_topc :::"open"::: ) ; end; theorem :: TOPGRP_1:54 (Bool "for" (Set (Var "G")) "being" ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a")) "holds" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k2_group_1 :::"""::: ) ))))) ; theorem :: TOPGRP_1:55 (Bool "for" (Set (Var "G")) "being" ($#l1_topgrp_1 :::"TopologicalGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" )) (Bool "ex" (Set (Var "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "a")) "st" (Bool (Set (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k1_group_2 :::"""::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))))) ; theorem :: TOPGRP_1:56 (Bool "for" (Set (Var "G")) "being" ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "A")) "being" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k1_group_2 :::"""::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; registrationlet "G" be ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "A" be ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); cluster (Set "A" ($#k1_group_2 :::"""::: ) ) -> ($#v1_tops_1 :::"dense"::: ) ; end; theorem :: TOPGRP_1:57 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "A")) "being" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set (Var "A"))) "is" ($#v1_tops_1 :::"dense"::: ) )))) ; theorem :: TOPGRP_1:58 (Bool "for" (Set (Var "G")) "being" ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::) (Bool "for" (Set (Var "A")) "being" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) "is" ($#v1_tops_1 :::"dense"::: ) )))) ; registrationlet "G" be ($#v4_topgrp_1 :::"BinContinuous"::: ) ($#l1_topgrp_1 :::"TopGroup":::); let "A" be ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "G")); cluster (Set "A" ($#k5_group_2 :::"*"::: ) "a") -> ($#v1_tops_1 :::"dense"::: ) ; cluster (Set "a" ($#k4_group_2 :::"*"::: ) "A") -> ($#v1_tops_1 :::"dense"::: ) ; end; theorem :: TOPGRP_1:59 (Bool "for" (Set (Var "G")) "being" ($#l1_topgrp_1 :::"TopologicalGroup":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "M")) "being" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "{" (Set "(" (Set (Var "V")) ($#k5_group_2 :::"*"::: ) (Set (Var "x")) ")" ) where V "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")), x "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) : (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) ")" ) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "G")))))) ; theorem :: TOPGRP_1:60 (Bool "for" (Set (Var "G")) "being" ($#l1_topgrp_1 :::"TopologicalGroup":::) "holds" (Bool (Set (Var "G")) "is" ($#v9_pre_topc :::"regular"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_topgrp_1 :::"UnContinuous"::: ) ($#v4_topgrp_1 :::"BinContinuous"::: ) -> ($#v9_pre_topc :::"regular"::: ) for ($#l1_topgrp_1 :::"TopGrStr"::: ) ; end; theorem :: TOPGRP_1:61 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ))) ;