:: The Definition and Basic Properties of Topological Groups :: by Artur Korni{\l}owicz :: :: Received September 7, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, SUBSET_1, PRE_TOPC, FUNCT_1, FUNCT_2, RELAT_1, VALUED_1, XBOOLE_0, ALGSTR_0, TARSKI, GROUP_1, ZFMISC_1, ORDINAL2, TOPS_2, CONNSP_2, TOPS_1, RCOMP_1, T_0TOPSP, BINOP_1, UNIALG_1, CARD_5, SETFAM_1, COMPTS_1, RLVECT_3, TOPGRP_1, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, SETFAM_1, GROUP_2, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_1, CONNSP_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP, CANTOR_1, YELLOW_8; constructors TOPS_1, TOPS_2, COMPTS_1, GROUP_2, BORSUK_1, GRCAT_1, URYSOHN1, T_0TOPSP, CANTOR_1, YELLOW_8, TEX_1; registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_1, GROUP_1, COMPTS_1, BORSUK_1, TEX_1, BORSUK_2, RELSET_1, CARD_1, ALGSTR_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve S, R for 1-sorted, X for Subset of R, T for TopStruct, x for set; registration let X be set; cluster one-to-one onto for Function of X, X; end; theorem :: TOPGRP_1:1 rng id S = [#]S; registration let R be 1-sorted; cluster (id R)/" -> one-to-one; end; theorem :: TOPGRP_1:2 (id R)/" = id R; theorem :: TOPGRP_1:3 (id R)"X = X; begin :: On the groups reserve H for non empty multMagma, P, Q, P1, Q1 for Subset of H, h for Element of H; theorem :: TOPGRP_1:4 P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1; theorem :: TOPGRP_1:5 P c= Q implies P * h c= Q * h; theorem :: TOPGRP_1:6 P c= Q implies h * P c= h * Q; reserve G for Group, A, B for Subset of G, a for Element of G; theorem :: TOPGRP_1:7 a in A" iff a" in A; ::$CT theorem :: TOPGRP_1:9 A c= B iff A" c= B"; theorem :: TOPGRP_1:10 (inverse_op G).:A = A"; theorem :: TOPGRP_1:11 (inverse_op G)"A = A"; theorem :: TOPGRP_1:12 inverse_op G is one-to-one; theorem :: TOPGRP_1:13 rng inverse_op G = the carrier of G; registration let G be Group; cluster inverse_op G -> one-to-one onto; end; theorem :: TOPGRP_1:14 (inverse_op G)" = inverse_op G; theorem :: TOPGRP_1:15 (the multF of H).:[:P,Q:] = P*Q; definition let G be non empty multMagma, a be Element of G; func a* -> Function of G, G means :: TOPGRP_1:def 1 for x being Element of G holds it.x = a * x; func *a -> Function of G, G means :: TOPGRP_1:def 2 for x being Element of G holds it.x = x * a; end; registration let G be Group, a be Element of G; cluster a* -> one-to-one onto; cluster *a -> one-to-one onto; end; theorem :: TOPGRP_1:16 h*.:P = h * P; theorem :: TOPGRP_1:17 (*h).:P = P * h; theorem :: TOPGRP_1:18 a*/" = a"*; theorem :: TOPGRP_1:19 (*a)/" = *(a"); begin :: On the topological spaces registration let T be TopStruct; cluster (id T)/" -> continuous; end; theorem :: TOPGRP_1:20 id T is being_homeomorphism; registration let T be non empty TopSpace, p be Point of T; cluster -> non empty for a_neighborhood of p; end; theorem :: TOPGRP_1:21 for T being non empty TopSpace, p being Point of T holds [#]T is a_neighborhood of p; registration let T be non empty TopSpace, p be Point of T; cluster non empty open for a_neighborhood of p; end; theorem :: TOPGRP_1:22 for S, T being non empty TopSpace, f being Function of S, T st f is open holds for p being Point of S, P being a_neighborhood of p ex R being open a_neighborhood of f.p st R c= f.:P; theorem :: TOPGRP_1:23 for S, T being non empty TopSpace, f being Function of S, T st for p being Point of S, P being open a_neighborhood of p ex R being a_neighborhood of f.p st R c= f.:P holds f is open; theorem :: TOPGRP_1:24 for S, T being non empty TopStruct, f being Function of S, T holds f is being_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one & for P being Subset of T holds P is closed iff f"P is closed; theorem :: TOPGRP_1:25 for S, T being non empty TopStruct, f being Function of S, T holds f is being_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one & for P being Subset of S holds P is open iff f.:P is open; theorem :: TOPGRP_1:26 for S, T being non empty TopStruct, f being Function of S, T holds f is being_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one & for P being Subset of T holds P is open iff f"P is open; theorem :: TOPGRP_1:27 for S being TopSpace, T being non empty TopSpace, f being Function of S, T holds f is continuous iff for P being Subset of T holds f"(Int P) c= Int(f "P); registration let T be non empty TopSpace; cluster non empty dense for Subset of T; end; theorem :: TOPGRP_1:28 for S, T being non empty TopSpace, f being Function of S, T, A being dense Subset of S st f is being_homeomorphism holds f.:A is dense; theorem :: TOPGRP_1:29 for S, T being non empty TopSpace, f being Function of S, T, A being dense Subset of T st f is being_homeomorphism holds f"A is dense; registration let S, T be TopStruct; cluster being_homeomorphism -> onto one-to-one continuous for Function of S, T; end; registration let S, T be non empty TopStruct; cluster being_homeomorphism -> open for Function of S, T; end; registration let T be TopStruct; cluster being_homeomorphism for Function of T, T; end; registration let T be TopStruct, f be being_homeomorphism Function of T, T; cluster f/" -> being_homeomorphism; end; begin :: The group of homoemorphisms definition let S,T be TopStruct; assume S,T are_homeomorphic; mode Homeomorphism of S,T -> Function of S,T means :: TOPGRP_1:def 3 it is being_homeomorphism; end; definition let T be TopStruct; mode Homeomorphism of T -> Function of T,T means :: TOPGRP_1:def 4 it is being_homeomorphism; end; definition let T be TopStruct; redefine mode Homeomorphism of T -> Homeomorphism of T,T; end; definition let T be TopStruct; redefine func id T -> Homeomorphism of T,T; end; definition let T be TopStruct; redefine func id T -> Homeomorphism of T; end; registration let T be TopStruct; cluster -> being_homeomorphism for Homeomorphism of T; end; theorem :: TOPGRP_1:30 for f being Homeomorphism of T holds f/" is Homeomorphism of T; theorem :: TOPGRP_1:31 for f, g being Homeomorphism of T holds f * g is Homeomorphism of T; definition let T be TopStruct; func HomeoGroup T -> strict multMagma means :: TOPGRP_1:def 5 (x in the carrier of it iff x is Homeomorphism of T) & for f, g being Homeomorphism of T holds (the multF of it).(f,g) = g * f; end; registration let T be TopStruct; cluster HomeoGroup T -> non empty; end; theorem :: TOPGRP_1:32 for f, g being Homeomorphism of T for a, b being Element of HomeoGroup T st f = a & g = b holds a * b = g * f; registration let T be TopStruct; cluster HomeoGroup T -> Group-like associative; end; theorem :: TOPGRP_1:33 id T = 1_HomeoGroup T; theorem :: TOPGRP_1:34 for f being Homeomorphism of T for a being Element of HomeoGroup T st f = a holds a" = f/"; definition let T be TopStruct; attr T is homogeneous means :: TOPGRP_1:def 6 for p, q being Point of T ex f being Homeomorphism of T st f.p = q; end; registration cluster -> homogeneous for 1-element TopStruct; end; theorem :: TOPGRP_1:35 for T being homogeneous non empty TopSpace st ex p being Point of T st {p} is closed holds T is T_1; theorem :: TOPGRP_1:36 for T being homogeneous non empty TopSpace st ex p being Point of T st for A being Subset of T st A is open & p in A holds ex B being Subset of T st p in B & B is open & Cl B c= A holds T is regular; begin :: On the topological groups definition struct (multMagma, TopStruct) TopGrStr (# carrier -> set, multF -> BinOp of the carrier, topology -> Subset-Family of the carrier #); end; registration let A be non empty set, R be BinOp of A, T be Subset-Family of A; cluster TopGrStr (#A, R, T#) -> non empty; end; registration let x be set, R be BinOp of {x}, T be Subset-Family of {x}; cluster TopGrStr (#{x}, R, T#) -> trivial; end; registration cluster -> Group-like associative commutative for 1-element multMagma; end; registration let a be set; cluster 1TopSp {a} -> trivial; end; registration cluster strict non empty for TopGrStr; end; registration cluster strict TopSpace-like 1-element for TopGrStr; end; :: definition :: let G be Group; :: redefine func inverse_op G -> Function of G, G; :: coherence; :: end; definition let G be Group-like associative non empty TopGrStr; attr G is UnContinuous means :: TOPGRP_1:def 7 inverse_op G is continuous; end; definition let G be TopSpace-like TopGrStr; attr G is BinContinuous means :: TOPGRP_1:def 8 for f being Function of [:G,G:], G st f = the multF of G holds f is continuous; end; registration cluster strict commutative UnContinuous BinContinuous for TopSpace-like Group-like associative 1-element TopGrStr; end; definition mode TopGroup is TopSpace-like Group-like associative non empty TopGrStr; end; definition mode TopologicalGroup is UnContinuous BinContinuous TopGroup; end; theorem :: TOPGRP_1:37 for T being BinContinuous non empty TopSpace-like TopGrStr, a, b being Element of T, W being a_neighborhood of a*b ex A being open a_neighborhood of a, B being open a_neighborhood of b st A*B c= W; theorem :: TOPGRP_1:38 for T being TopSpace-like non empty TopGrStr st (for a, b being Element of T, W being a_neighborhood of a*b ex A being a_neighborhood of a, B being a_neighborhood of b st A*B c= W) holds T is BinContinuous; theorem :: TOPGRP_1:39 for T being UnContinuous TopGroup, a being Element of T, W being a_neighborhood of a" ex A being open a_neighborhood of a st A" c= W; theorem :: TOPGRP_1:40 for T being TopGroup st for a being Element of T, W being a_neighborhood of a" ex A being a_neighborhood of a st A" c= W holds T is UnContinuous; theorem :: TOPGRP_1:41 for T being TopologicalGroup, a, b being Element of T for W being a_neighborhood of a*(b") ex A being open a_neighborhood of a, B being open a_neighborhood of b st A*(B") c= W; theorem :: TOPGRP_1:42 for T being TopGroup st for a, b being Element of T, W being a_neighborhood of a*(b") ex A being a_neighborhood of a, B being a_neighborhood of b st A*(B") c= W holds T is TopologicalGroup; registration let G be BinContinuous non empty TopSpace-like TopGrStr, a be Element of G; cluster a* -> continuous; cluster *a -> continuous; end; theorem :: TOPGRP_1:43 for G being BinContinuous TopGroup, a being Element of G holds a * is Homeomorphism of G; theorem :: TOPGRP_1:44 for G being BinContinuous TopGroup, a being Element of G holds * a is Homeomorphism of G; definition let G be BinContinuous TopGroup, a be Element of G; redefine func a* -> Homeomorphism of G; redefine func *a -> Homeomorphism of G; end; theorem :: TOPGRP_1:45 for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G; definition let G be UnContinuous TopGroup; redefine func inverse_op G -> Homeomorphism of G; end; registration cluster BinContinuous -> homogeneous for TopGroup; end; theorem :: TOPGRP_1:46 for G being BinContinuous TopGroup, F being closed Subset of G, a being Element of G holds F * a is closed; theorem :: TOPGRP_1:47 for G being BinContinuous TopGroup, F being closed Subset of G, a being Element of G holds a * F is closed; registration let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G; cluster F * a -> closed; cluster a * F -> closed; end; theorem :: TOPGRP_1:48 for G being UnContinuous TopGroup, F being closed Subset of G holds F" is closed; registration let G be UnContinuous TopGroup, F be closed Subset of G; cluster F" -> closed; end; theorem :: TOPGRP_1:49 for G being BinContinuous TopGroup, O being open Subset of G, a being Element of G holds O * a is open; theorem :: TOPGRP_1:50 for G being BinContinuous TopGroup, O being open Subset of G, a being Element of G holds a * O is open; registration let G be BinContinuous TopGroup, A be open Subset of G, a be Element of G; cluster A * a -> open; cluster a * A -> open; end; theorem :: TOPGRP_1:51 for G being UnContinuous TopGroup, O being open Subset of G holds O" is open; registration let G be UnContinuous TopGroup, A be open Subset of G; cluster A" -> open; end; theorem :: TOPGRP_1:52 for G being BinContinuous TopGroup, A, O being Subset of G st O is open holds O * A is open; theorem :: TOPGRP_1:53 for G being BinContinuous TopGroup, A, O being Subset of G st O is open holds A * O is open; registration let G be BinContinuous TopGroup, A be open Subset of G, B be Subset of G; cluster A * B -> open; cluster B * A -> open; end; theorem :: TOPGRP_1:54 for G being UnContinuous TopGroup, a being Point of G, A being a_neighborhood of a holds A" is a_neighborhood of a"; theorem :: TOPGRP_1:55 for G being TopologicalGroup, a being Point of G, A being a_neighborhood of a*a" ex B being open a_neighborhood of a st B*B" c= A; theorem :: TOPGRP_1:56 for G being UnContinuous TopGroup, A being dense Subset of G holds A" is dense; registration let G be UnContinuous TopGroup, A be dense Subset of G; cluster A" -> dense; end; theorem :: TOPGRP_1:57 for G being BinContinuous TopGroup, A being dense Subset of G, a being Point of G holds a*A is dense; theorem :: TOPGRP_1:58 for G being BinContinuous TopGroup, A being dense Subset of G, a being Point of G holds A*a is dense; registration let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G; cluster A * a -> dense; cluster a * A -> dense; end; theorem :: TOPGRP_1:59 for G being TopologicalGroup, B being Basis of 1_G, M being dense Subset of G holds { V * x where V is Subset of G, x is Point of G: V in B & x in M } is Basis of G; theorem :: TOPGRP_1:60 for G being TopologicalGroup holds G is regular; registration cluster -> regular for TopologicalGroup; end; theorem :: TOPGRP_1:61 for T being TopStruct, f be Function of T,T st T is empty holds f is being_homeomorphism;