:: The Definition and Basic Properties of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received September 7, 1998
:: Copyright (c) 1998-2018 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, NUMERALS;
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;