Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### The Definition and Basic Properties of Topological Groups

**by****Artur Kornilowicz**- Received September 7, 1998
- MML identifier: TOPGRP_1

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, SGRAPH1, FUNCT_1, RELAT_1, SUBSET_1, VECTSP_1, REALSET1, GROUP_1, ORDINAL2, TOPS_2, CONNSP_2, TOPS_1, BOOLE, FUNCT_2, BINOP_1, UNIALG_1, URYSOHN1, COMPTS_1, SETFAM_1, PCOMPS_1, TARSKI, TOPGRP_1, RLVECT_3, SEQ_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, TOPS_2, FUNCT_1, PARTFUN1, BINOP_1, SETFAM_1, GRCAT_1, REALSET1, GROUP_1, GROUP_2, STRUCT_0, VECTSP_1, PRE_TOPC, TOPS_1, COMPTS_1, PCOMPS_1, URYSOHN1, BORSUK_1, T_0TOPSP, CANTOR_1, FUNCT_2, YELLOW_8; constructors REALSET1, TOPS_1, TOPS_2, GRCAT_1, T_0TOPSP, GROUP_7, URYSOHN1, COMPTS_1, CANTOR_1, YELLOW_8, MEMBERED; clusters BORSUK_1, BORSUK_2, STRUCT_0, GROUP_1, PRE_TOPC, WAYBEL10, TEX_1, PCOMPS_1, TOPS_1, RELSET_1, SUBSET_1, FUNCT_2, PARTFUN1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve S for 1-sorted, R for non empty 1-sorted, X for Subset of R, T for non empty TopStruct, x for set; definition let X be set; cluster one-to-one onto Function of X, X; end; theorem :: TOPGRP_1:1 rng id S = [#]S; definition let R be non empty 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; definition let S be 1-sorted; cluster one-to-one onto map of S, S; end; begin :: On the groups reserve H for non empty HGrStr, 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; theorem :: TOPGRP_1:8 A"" = A; 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; definition 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 mult of H).:[:P,Q:] = P*Q; definition let G be non empty HGrStr, a be Element of G; func a* -> map of G, G means :: TOPGRP_1:def 1 for x being Element of G holds it.x = a * x; func *a -> map of G, G means :: TOPGRP_1:def 2 for x being Element of G holds it.x = x * a; end; definition 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 definition let T be non empty TopStruct; cluster (id T)/" -> continuous; end; theorem :: TOPGRP_1:20 id T is_homeomorphism; definition let T be non empty TopSpace, p be Point of T; cluster -> non empty 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; definition let T be non empty TopSpace, p be Point of T; cluster non empty open a_neighborhood of p; end; theorem :: TOPGRP_1:22 for S, T being non empty TopSpace, f being map 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 map 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 map of S, T holds f is_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 map of S, T holds f is_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 map of S, T holds f is_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 map of S, T holds f is continuous iff for P being Subset of T holds f"(Int P) c= Int(f"P); definition let T be non empty TopSpace; cluster non empty dense Subset of T; end; theorem :: TOPGRP_1:28 for S, T being non empty TopSpace, f being map of S, T, A being dense Subset of S st f is_homeomorphism holds f.:A is dense; theorem :: TOPGRP_1:29 for S, T being non empty TopSpace, f being map of S, T, A being dense Subset of T st f is_homeomorphism holds f"A is dense; definition let S, T be non empty TopStruct; cluster being_homeomorphism -> onto one-to-one continuous open map of S, T; end; definition let T be non empty TopStruct; cluster being_homeomorphism map of T, T; end; definition let T be non empty TopStruct, f be being_homeomorphism map of T, T; cluster f/" -> being_homeomorphism; end; begin :: The group of homoemorphisms definition let T be non empty TopStruct; mode Homeomorphism of T -> map of T, T means :: TOPGRP_1:def 3 it is_homeomorphism; end; definition let T be non empty TopStruct; redefine func id T -> Homeomorphism of T; end; definition let T be non empty TopStruct; cluster -> being_homeomorphism 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 non empty TopStruct; func HomeoGroup T -> strict HGrStr means :: TOPGRP_1:def 4 (x in the carrier of it iff x is Homeomorphism of T) & for f, g being Homeomorphism of T holds (the mult of it).(f,g) = g * f; end; definition let T be non empty 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; definition let T be non empty 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 non empty TopStruct; attr T is homogeneous means :: TOPGRP_1:def 5 for p, q being Point of T ex f being Homeomorphism of T st f.p = q; end; definition cluster trivial -> homogeneous (non empty TopStruct); end; definition cluster strict trivial non empty TopSpace; 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_T1; 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_T3; begin :: On the topological groups definition struct (HGrStr, TopStruct) TopGrStr (# carrier -> set, mult -> BinOp of the carrier, topology -> Subset-Family of the carrier #); end; definition 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; definition let x be set, R be BinOp of {x}, T be Subset-Family of {x}; cluster TopGrStr (#{x}, R, T#) -> trivial; end; definition cluster trivial -> Group-like associative commutative (non empty HGrStr); end; definition let a be set; cluster 1TopSp {a} -> trivial; end; definition cluster strict non empty TopGrStr; end; definition cluster strict TopSpace-like trivial (non empty TopGrStr); end; definition let G be Group-like associative (non empty TopGrStr); redefine func inverse_op G -> map of G, G; end; definition let G be Group-like associative (non empty TopGrStr); attr G is UnContinuous means :: TOPGRP_1:def 6 inverse_op G is continuous; end; definition let G be TopSpace-like TopGrStr; attr G is BinContinuous means :: TOPGRP_1:def 7 for f being map of [:G,G:], G st f = the mult of G holds f is continuous; end; definition cluster strict commutative trivial UnContinuous BinContinuous (TopSpace-like Group-like associative (non empty 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; definition 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; definition cluster BinContinuous -> homogeneous 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; definition 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; definition 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; definition 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; definition 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; definition 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; definition 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; definition 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_T3; definition cluster -> being_T3 TopologicalGroup; end;

Back to top