:: The Definition and Basic Properties of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received September 7, 1998
:: Copyright (c) 1998-2026 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;
definitions TARSKI, FUNCT_1, PRE_TOPC, GROUP_1, STRUCT_0, TOPS_1, TOPS_2,
CONNSP_2, FUNCT_2, T_0TOPSP, XBOOLE_0;
equalities STRUCT_0, XBOOLE_0, BINOP_1, SUBSET_1, COMPTS_1, RELAT_1, ALGSTR_0,
GROUP_2;
expansions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, FUNCT_2, T_0TOPSP, RELAT_1;
theorems PRE_TOPC, RELAT_1, TOPS_1, TOPS_2, BINOP_1, FUNCT_2, GROUP_1,
GROUP_2, TARSKI, FUNCT_1, BORSUK_1, TEX_2, ZFMISC_1, CONNSP_2, URYSOHN1,
T_0TOPSP, YELLOW_8, YELLOW_9, XBOOLE_0, XBOOLE_1, STRUCT_0, RELSET_1;
schemes BINOP_1, FUNCT_2, XBOOLE_0;
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;
existence
proof
take id X;
thus id X is one-to-one;
thus rng id X = X by RELAT_1:45;
end;
end;
theorem
rng id S = [#]S by RELAT_1:45;
registration
let R be 1-sorted;
cluster (id R)/" -> one-to-one;
coherence
proof
rng (id R) = [#]R by RELAT_1:45;
hence thesis by TOPS_2:50;
end;
end;
theorem Th2:
(id R)/" = id R
proof
rng (id R) = [#]R by RELAT_1:45;
then id R is onto;
hence (id R)/" = (id the carrier of R)" by TOPS_2:def 4
.= id R by FUNCT_1:45;
end;
theorem
(id R)"X = X
proof
rng id R = [#]R by RELAT_1:45;
then
A1: (id R).:X = ((id R)/")"X by TOPS_2:54;
(id R)/" = id R by Th2;
hence thesis by A1,FUNCT_1:92;
end;
begin :: On the groups
reserve H for non empty multMagma,
P, Q, P1, Q1 for Subset of H,
h for Element of H;
theorem Th4:
P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1
proof
assume
A1: P c= P1 & Q c= Q1;
let x be object;
assume x in P * Q;
then ex g, t being Element of H st x = g * t & g in P & t in Q;
hence thesis by A1;
end;
theorem Th5:
P c= Q implies P * h c= Q * h
proof
assume
A1: P c= Q;
let x be object;
assume x in P * h;
then ex g being Element of H st x = g * h & g in P by GROUP_2:28;
hence thesis by A1,GROUP_2:28;
end;
theorem
P c= Q implies h * P c= h * Q
proof
assume
A1: P c= Q;
let x be object;
assume x in h * P;
then ex g being Element of H st x = h * g & g in P by GROUP_2:27;
hence thesis by A1,GROUP_2:27;
end;
reserve G for Group,
A, B for Subset of G,
a for Element of G;
theorem Th7:
a in A" iff a" in A
proof
a"" = a & A"" = A;
hence thesis;
end;
Lm1: A c= B implies A" c= B"
proof
assume
A1: A c= B;
let a be object;
assume a in A";
then ex g being Element of G st a = g" & g in A;
hence thesis by A1;
end;
::$CT
theorem Th8:
A c= B iff A" c= B"
proof
A"" = A & B"" = B;
hence thesis by Lm1;
end;
theorem Th9:
(inverse_op G).:A = A"
proof
set f = inverse_op G;
hereby
let y be object;
assume y in f.:A;
then consider x being object such that
A1: x in the carrier of G and
A2: x in A and
A3: y = f.x by FUNCT_2:64;
reconsider x as Element of G by A1;
y = x" by A3,GROUP_1:def 6;
hence y in A" by A2;
end;
let y be object;
assume y in A";
then consider g being Element of G such that
A4: y = g" & g in A;
f.g = g" by GROUP_1:def 6;
hence thesis by A4,FUNCT_2:35;
end;
theorem Th10:
(inverse_op G)"A = A"
proof
set f = inverse_op G;
A1: dom f = the carrier of G by FUNCT_2:def 1;
hereby
let x be object;
assume
A2: x in f"A;
then reconsider g = x as Element of G;
f.x in A by A2,FUNCT_1:def 7;
then (f.g)" in A";
then g"" in A" by GROUP_1:def 6;
hence x in A";
end;
let x be object;
assume x in A";
then consider g being Element of G such that
A3: x = g" & g in A;
f.(g") = g"" by GROUP_1:def 6
.= g;
hence thesis by A1,A3,FUNCT_1:def 7;
end;
theorem Th11:
inverse_op G is one-to-one
proof
set f = inverse_op G;
let x1, x2 be object;
assume that
A1: x1 in dom f & x2 in dom f and
A2: f.x1 = f.x2;
reconsider a = x1, b = x2 as Element of G by A1;
f.a = a" & f.b = b" by GROUP_1:def 6;
hence thesis by A2,GROUP_1:9;
end;
theorem Th12:
rng inverse_op G = the carrier of G
proof
set f = inverse_op G;
thus rng f c= the carrier of G;
let x be object;
A1: dom f = the carrier of G by FUNCT_2:def 1;
assume x in the carrier of G;
then reconsider a = x as Element of G;
f.(a") = a"" by GROUP_1:def 6
.= a;
hence thesis by A1,FUNCT_1:def 3;
end;
registration
let G be Group;
cluster inverse_op G -> one-to-one onto;
coherence
by Th11,Th12;
end;
theorem Th13:
(inverse_op G)" = inverse_op G
proof
set f = inverse_op G;
A1: dom f = the carrier of G by FUNCT_2:def 1;
A2: now
let x be object;
assume x in dom f;
then reconsider g = x as Element of G;
A3: f.(g") = g"" by GROUP_1:def 6
.= g;
thus f.x = g" by GROUP_1:def 6
.= f".x by A1,A3,FUNCT_1:32;
end;
thus thesis by A1,A2;
end;
theorem Th14:
(the multF of H).:[:P,Q:] = P*Q
proof
set f = the multF of H;
hereby
let y be object;
assume y in f.:[:P,Q:];
then consider x being object such that
x in [:the carrier of H,the carrier of H:] and
A1: x in [:P,Q:] and
A2: y = f.x by FUNCT_2:64;
consider a, b being object such that
A3: a in P & b in Q and
A4: x = [a,b] by A1,ZFMISC_1:def 2;
reconsider a, b as Element of H by A3;
y = a*b by A2,A4;
hence y in P*Q by A3;
end;
let y be object;
assume y in P*Q;
then consider g, h being Element of H such that
A5: y = g*h and
A6: g in P & h in Q;
[g,h] in [:P,Q:] by A6,ZFMISC_1:87;
hence thesis by A5,FUNCT_2:35;
end;
definition
let G be non empty multMagma, a be Element of G;
func a* -> Function of G, G means
:Def1:
for x being Element of G holds it.x = a * x;
existence
proof
deffunc U(Element of G) = a * $1;
consider f being Function of the carrier of G, the carrier of G such that
A1: for x being Element of G holds f.x = U(x) from FUNCT_2:sch 4;
reconsider f as Function of G, G;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f, g be Function of G, G such that
A2: for x being Element of G holds f.x = a * x and
A3: for x being Element of G holds g.x = a * x;
now
let x be object;
assume x in the carrier of G;
then reconsider y = x as Element of G;
thus f.x = a * y by A2
.= g.x by A3;
end;
hence thesis;
end;
func *a -> Function of G, G means
:Def2:
for x being Element of G holds it.x = x * a;
existence
proof
deffunc U(Element of G) = $1 *a;
consider f being Function of the carrier of G, the carrier of G such that
A4: for x being Element of G holds f.x = U(x) from FUNCT_2:sch 4;
reconsider f as Function of G, G;
take f;
thus thesis by A4;
end;
uniqueness
proof
let f, g be Function of G, G such that
A5: for x being Element of G holds f.x = x * a and
A6: for x being Element of G holds g.x = x * a;
now
let x be object;
assume x in the carrier of G;
then reconsider y = x as Element of G;
thus f.x = y * a by A5
.= g.x by A6;
end;
hence thesis;
end;
end;
registration
let G be Group, a be Element of G;
cluster a* -> one-to-one onto;
coherence
proof
set f = a*;
A1: dom f = the carrier of G by FUNCT_2:def 1;
hereby
let x1, x2 be object;
assume that
A2: x1 in dom f & x2 in dom f and
A3: f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of G by A2;
A4: f.y1 = a * y1 & f.y2 = a * y2 by Def1;
thus x1 = 1_G * y1 by GROUP_1:def 4
.= a" * a * y1 by GROUP_1:def 5
.= a" * (a * y1) by GROUP_1:def 3
.= a" * a * y2 by A3,A4,GROUP_1:def 3
.= 1_G * y2 by GROUP_1:def 5
.= x2 by GROUP_1:def 4;
end;
thus rng f c= the carrier of G;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
f.(a"*y1) = a * (a" * y1) by Def1
.= a * (a") * y1 by GROUP_1:def 3
.= 1_G * y1 by GROUP_1:def 5
.= y by GROUP_1:def 4;
hence thesis by A1,FUNCT_1:def 3;
end;
cluster *a -> one-to-one onto;
coherence
proof
set f = *a;
A5: dom f = the carrier of G by FUNCT_2:def 1;
hereby
let x1, x2 be object;
assume that
A6: x1 in dom f & x2 in dom f and
A7: f.x1 = f.x2;
reconsider y1 = x1, y2 = x2 as Element of G by A6;
A8: f.y1 = y1 * a & f.y2 = y2 * a by Def2;
thus x1 = y1 * 1_G by GROUP_1:def 4
.= y1 * (a * a") by GROUP_1:def 5
.= y1 * a * a" by GROUP_1:def 3
.= y2 * (a * a") by A7,A8,GROUP_1:def 3
.= y2 * 1_G by GROUP_1:def 5
.= x2 by GROUP_1:def 4;
end;
thus rng f c= the carrier of G;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
f.(y1*a") = y1 * a" * a by Def2
.= y1 * (a" * a) by GROUP_1:def 3
.= y1 * 1_G by GROUP_1:def 5
.= y by GROUP_1:def 4;
hence thesis by A5,FUNCT_1:def 3;
end;
end;
theorem Th15:
h*.:P = h * P
proof
set f = h*;
hereby
let y be object;
assume y in f.:P;
then consider x being object such that
A1: x in dom f and
A2: x in P & y = f.x by FUNCT_1:def 6;
reconsider x as Element of H by A1;
f.x = h * x by Def1;
hence y in h * P by A2,GROUP_2:27;
end;
let y be object;
assume y in h * P;
then consider s being Element of H such that
A3: y = h * s & s in P by GROUP_2:27;
dom f = the carrier of H & f.s = h * s by Def1,FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 6;
end;
theorem Th16:
(*h).:P = P * h
proof
set f = *h;
hereby
let y be object;
assume y in f.:P;
then consider x being object such that
A1: x in dom f and
A2: x in P & y = f.x by FUNCT_1:def 6;
reconsider x as Element of H by A1;
f.x = x * h by Def2;
hence y in P * h by A2,GROUP_2:28;
end;
let y be object;
assume y in P * h;
then consider s being Element of H such that
A3: y = s * h & s in P by GROUP_2:28;
dom f = the carrier of H & f.s = s * h by Def2,FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 6;
end;
theorem Th17:
a*/" = a"*
proof
set f = a*, g = a"*;
A1: now
reconsider h = f as Function;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
rng f = the carrier of G by FUNCT_2:def 3;
then
A2: y1 in rng f;
dom f = the carrier of G by FUNCT_2:def 1;
then
A3: g.y1 in dom f & f/".y1 in dom f;
f.(g.y) = a*(g.y1) by Def1
.= a*(a"*y1) by Def1
.= a*a"*y1 by GROUP_1:def 3
.= 1_G*y1 by GROUP_1:def 5
.= y by GROUP_1:def 4
.= h.(h".y) by A2,FUNCT_1:35
.= f.(f/".y) by TOPS_2:def 4;
hence f/".y = g.y by A3,FUNCT_1:def 4;
end;
thus thesis by A1;
end;
theorem Th18:
(*a)/" = *(a")
proof
set f = *a, g = *(a");
A1: now
reconsider h = f as Function;
let y be object;
assume y in the carrier of G;
then reconsider y1 = y as Element of G;
rng f = the carrier of G by FUNCT_2:def 3;
then
A2: y1 in rng f;
dom f = the carrier of G by FUNCT_2:def 1;
then
A3: g.y1 in dom f & f/".y1 in dom f;
f.(g.y) = (g.y1)*a by Def2
.= y1*a"*a by Def2
.= y1*(a"*a) by GROUP_1:def 3
.= y1*(1_G) by GROUP_1:def 5
.= y by GROUP_1:def 4
.= h.(h".y) by A2,FUNCT_1:35
.= f.(f/".y) by TOPS_2:def 4;
hence f/".y = g.y by A3,FUNCT_1:def 4;
end;
thus thesis by A1;
end;
begin :: On the topological spaces
registration
let T be TopStruct;
cluster (id T)/" -> continuous;
coherence by Th2;
end;
theorem Th19:
id T is being_homeomorphism
by RELAT_1:45;
registration
let T be non empty TopSpace, p be Point of T;
cluster -> non empty for a_neighborhood of p;
coherence
proof
let N be a_neighborhood of p;
p in Int N by CONNSP_2:def 1;
hence thesis;
end;
end;
theorem Th20:
for T being non empty TopSpace, p being Point of T holds [#]T is
a_neighborhood of p
proof
let T be non empty TopSpace, p be Point of T;
Int [#]T = the carrier of T by TOPS_1:15;
hence p in Int [#]T;
end;
registration
let T be non empty TopSpace, p be Point of T;
cluster non empty open for a_neighborhood of p;
existence
proof
reconsider B = [#]T as a_neighborhood of p by Th20;
take B;
thus thesis;
end;
end;
theorem
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
proof
let S, T be non empty TopSpace, f be Function of S, T such that
A1: for A being Subset of S st A is open holds f.:A is open;
let p be Point of S, P be a_neighborhood of p;
A2: p in Int P by CONNSP_2:def 1;
f.:Int P is open by A1;
then reconsider R = f.:Int P as open a_neighborhood of f.p by A2,CONNSP_2:3
,FUNCT_2:35;
take R;
thus thesis by RELAT_1:123,TOPS_1:16;
end;
theorem
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
proof
let S, T be non empty TopSpace, f be Function of S, T such that
A1: 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;
let A be Subset of S such that
A2: A is open;
for x being set holds x in f.:A iff ex Q being Subset of T st Q is open
& Q c= f.:A & x in Q
proof
let x be set;
hereby
assume x in f.:A;
then consider a being object such that
A3: a in dom f and
A4: a in A and
A5: x = f.a by FUNCT_1:def 6;
reconsider p = a as Point of S by A3;
consider V being Subset of S such that
A6: V is open and
A7: V c= A and
A8: a in V by A2,A4;
V is a_neighborhood of p by A6,A8,CONNSP_2:3;
then consider R being a_neighborhood of f.p such that
A9: R c= f.:V by A1,A6;
take K = Int R;
Int R c= R by TOPS_1:16;
then
A10: K c= f.:V by A9;
thus K is open;
f.:V c= f.:A by A7,RELAT_1:123;
hence K c= f.:A by A10;
thus x in K by A5,CONNSP_2:def 1;
end;
thus thesis;
end;
hence thesis by TOPS_1:25;
end;
theorem
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
proof
let S, T be non empty TopStruct, f be Function of S, T;
hereby
assume
A1: f is being_homeomorphism;
hence
A2: dom f = [#]S & rng f = [#]T & f is one-to-one;
let P be Subset of T;
hereby
assume
A3: P is closed;
f is continuous by A1;
hence f"P is closed by A3;
end;
assume f"P is closed;
then f.:(f"P) is closed by A1,TOPS_2:58;
hence P is closed by A2,FUNCT_1:77;
end;
assume that
A4: dom f = [#]S and
A5: rng f = [#]T and
A6: f is one-to-one and
A7: for P being Subset of T holds P is closed iff f"P is closed;
thus dom f = [#]S & rng f = [#]T & f is one-to-one by A4,A5,A6;
thus f is continuous
by A7;
let R be Subset of S such that
A8: R is closed;
for x1, x2 being Element of S st x1 in R & f.x1 = f.x2 holds x2 in R by A4,A6
;
then
A9: f"(f.:R) = R by T_0TOPSP:1;
(f/")"R = f.:R by A5,A6,TOPS_2:54;
hence thesis by A7,A8,A9;
end;
theorem Th24:
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
proof
let S, T be non empty TopStruct, f be Function of S, T;
A1: [#]T <> {};
A2: [#]S <> {};
hereby
assume
A3: f is being_homeomorphism;
hence
A4: dom f = [#]S & rng f = [#]T & f is one-to-one;
let P be Subset of S;
A5: f"(f.:P) c= P & P c= f"(f.:P) by A4,FUNCT_1:76,82;
A6: f/" is continuous by A3;
hereby
assume
A7: P is open;
f is onto by A4;
then (f/")"P = ((f qua Function)")"P by A4,TOPS_2:def 4
.= f.:P by A4,FUNCT_1:84;
hence f.:P is open by A2,A6,A7,TOPS_2:43;
end;
assume
A8: f.:P is open;
f is continuous by A3;
then f"(f.:P) is open by A1,A8,TOPS_2:43;
hence P is open by A5,XBOOLE_0:def 10;
end;
assume that
A9: dom f = [#]S and
A10: rng f = [#]T and
A11: f is one-to-one and
A12: for P being Subset of S holds P is open iff f.:P is open;
now
let B be Subset of T such that
A13: B is open;
B = f.:f"B by A10,FUNCT_1:77;
hence f"B is open by A12,A13;
end;
then
A14: f is continuous by A1,TOPS_2:43;
now
let B be Subset of S such that
A15: B is open;
f is onto by A10;
then (f/")"B = ((f qua Function)")"B by A11,TOPS_2:def 4
.= f.:B by A11,FUNCT_1:84;
hence f/""B is open by A12,A15;
end;
then f/" is continuous by A2,TOPS_2:43;
hence thesis by A9,A10,A11,A14;
end;
theorem
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
proof
let S, T be non empty TopStruct, f be Function of S, T;
A1: [#]T <> {};
hereby
assume
A2: f is being_homeomorphism;
hence
A3: dom f = [#]S & rng f = [#]T & f is one-to-one;
let P be Subset of T;
thus P is open implies f"P is open by A2,TOPS_2:43;
assume f"P is open;
then f.:(f"P) is open by A2,Th24;
hence P is open by A3,FUNCT_1:77;
end;
assume that
A4: dom f = [#]S and
A5: rng f = [#]T and
A6: f is one-to-one and
A7: for P being Subset of T holds P is open iff f"P is open;
A8: now
let R be Subset of S such that
A9: R is open;
for x1, x2 being Element of S st x1 in R & f.x1 = f.x2 holds x2 in R
by A4,A6;
then
A10: f"(f.:R) = R by T_0TOPSP:1;
(f/")"R = f.:R by A5,A6,TOPS_2:54;
hence (f/")"R is open by A7,A9,A10;
end;
thus dom f = [#]S & rng f = [#]T & f is one-to-one by A4,A5,A6;
thus f is continuous by A1,A7,TOPS_2:43;
[#]S <> {};
hence thesis by A8,TOPS_2:43;
end;
theorem
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)
proof
let S be TopSpace, T be non empty TopSpace, f be Function of S, T;
A1: [#]T <> {};
hereby
assume
A2: f is continuous;
let P be Subset of T;
f"Int P c= f"P by RELAT_1:143,TOPS_1:16;
then
A3: Int(f"Int P) c= Int(f"P) by TOPS_1:19;
f"(Int P) is open by A1,A2,TOPS_2:43;
hence f"(Int P) c= Int(f"P) by A3,TOPS_1:23;
end;
assume
A4: for P being Subset of T holds f"(Int P) c= Int(f"P);
now
let P be Subset of T;
assume P is open;
then Int P = P by TOPS_1:23;
then
A5: f"P c= Int (f"P) by A4;
Int (f"P) c= f"P by TOPS_1:16;
hence f"P is open by A5,XBOOLE_0:def 10;
end;
hence thesis by A1,TOPS_2:43;
end;
registration
let T be non empty TopSpace;
cluster non empty dense for Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
theorem Th27:
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
proof
let S, T be non empty TopSpace, f be Function of S, T, A be dense Subset of
S such that
A1: f is being_homeomorphism;
A2: rng f = [#]T by A1;
Cl A = [#]S by TOPS_1:def 3;
hence Cl (f.:A) = f.:the carrier of S by A1,TOPS_2:60
.= [#]T by A2,RELSET_1:22;
end;
theorem Th28:
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
proof
let S, T be non empty TopSpace, f be Function of S, T, A be dense Subset of
T such that
A1: f is being_homeomorphism;
A2: Cl A = [#]T by TOPS_1:def 3;
thus Cl (f"A) = f"(Cl A) by A1,TOPS_2:59
.= [#]S by A2,TOPS_2:41;
end;
registration
let S, T be TopStruct;
cluster being_homeomorphism -> onto one-to-one continuous for
Function of S, T;
coherence;
end;
registration
let S, T be non empty TopStruct;
cluster being_homeomorphism -> open for Function of S, T;
coherence
by Th24;
end;
registration
let T be TopStruct;
cluster being_homeomorphism for Function of T, T;
existence
proof
take id T;
thus thesis by Th19;
end;
end;
registration
let T be TopStruct, f be being_homeomorphism Function of T, T;
cluster f/" -> being_homeomorphism;
coherence
proof
per cases;
suppose
T is non empty;
hence thesis by TOPS_2:56;
end;
suppose
T is empty;
then
A1: the carrier of T is empty;
f/" = f" by TOPS_2:def 4
.= id T by A1;
hence thesis by Th19;
end;
end;
end;
begin :: The group of homoemorphisms
definition
let S,T be TopStruct;
assume
A1: S,T are_homeomorphic;
mode Homeomorphism of S,T -> Function of S,T means
:Def3:
it is being_homeomorphism;
existence by A1;
end;
definition
let T be TopStruct;
mode Homeomorphism of T -> Function of T,T means
:Def4:
it is being_homeomorphism;
existence
proof
A1: id T is being_homeomorphism by Th19;
then T,T are_homeomorphic;
then reconsider f = id T as Homeomorphism of T,T by A1,Def3;
f is being_homeomorphism by Th19;
hence thesis;
end;
end;
definition
let T be TopStruct;
redefine mode Homeomorphism of T -> Homeomorphism of T,T; :: redefines Homeomorphism (TOPGRP_1, definition)
coherence
proof
let f be Homeomorphism of T;
A1: f is being_homeomorphism by Def4;
then T,T are_homeomorphic;
hence thesis by A1,Def3;
end;
end;
definition
let T be TopStruct;
redefine func id T -> Homeomorphism of T,T; :: redefines id (STRUCT_0, definition)
coherence
proof
id T is being_homeomorphism by Th19;
hence T,T are_homeomorphic;
thus thesis by Th19;
end;
end;
definition
let T be TopStruct;
redefine func id T -> Homeomorphism of T; :: redefines id (STRUCT_0, definition)
coherence
proof
thus id T is being_homeomorphism by Th19;
end;
end;
registration
let T be TopStruct;
cluster -> being_homeomorphism for Homeomorphism of T;
coherence by Def4;
end;
theorem Th29:
for f being Homeomorphism of T holds f/" is Homeomorphism of T
proof
let f be Homeomorphism of T;
thus f/" is being_homeomorphism;
end;
Lm2: for T being TopStruct, f be Function of T,T st T is empty holds f is
being_homeomorphism
proof
let T be TopStruct;
let f be Function of T,T;
assume
A1: T is empty;
then f = {} .= id T by A1;
hence thesis;
end;
theorem Th30:
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
proof
let f, g be Homeomorphism of T;
T is non empty or T is empty;
hence f*g is being_homeomorphism by TOPS_2:57;
end;
definition
let T be TopStruct;
func HomeoGroup T -> strict multMagma means
:Def5:
(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;
existence
proof
defpred X[object] means $1 is Homeomorphism of T;
consider A being set such that
A1: for q being object holds q in A iff q in Funcs(the carrier of T,the
carrier of T) & X[q] from XBOOLE_0:sch 1;
A2: for f being Homeomorphism of T holds f in A by A1, FUNCT_2:9;
then reconsider A as non empty set;
defpred P[Element of A, Element of A, Element of A] means ex f, g being
Homeomorphism of T st $1 = f & $2 = g & $3 = g * f;
A3: for x, y being Element of A ex z being Element of A st P[x,y,z]
proof
let x, y be Element of A;
reconsider x1 = x, y1 = y as Homeomorphism of T by A1;
y1 * x1 is Homeomorphism of T by Th30;
then reconsider z = y1 * x1 as Element of A by A2;
take z, x1, y1;
thus thesis;
end;
consider o being BinOp of A such that
A4: for a, b being Element of A holds P[a,b,o.(a,b)] from BINOP_1:sch
3(A3 );
take G = multMagma (#A, o#);
let x;
thus x in the carrier of G iff x is Homeomorphism of T by A1,A2;
let f, g be Homeomorphism of T;
reconsider f1 = f, g1 = g as Element of A by A2;
ex m, n being Homeomorphism of T st f1 = m & g1 = n & o.(f1,g1) = n *
m by A4;
hence thesis;
end;
uniqueness
proof
defpred X[object] means $1 is Homeomorphism of T;
let A, B be strict multMagma;
assume that
A5: (x in the carrier of A iff x is Homeomorphism of T) & for f, g
being Homeomorphism of T holds (the multF of A).(f,g) = g * f and
A6: (x in the carrier of B iff x is Homeomorphism of T) & for f, g
being Homeomorphism of T holds (the multF of B).(f,g) = g * f;
A7: for x being object holds x in the carrier of B iff X[x] by A6;
A8: for c, d being set st c in the carrier of A & d in the carrier of A
holds (the multF of A).(c,d) = (the multF of B).(c,d)
proof
let c, d be set;
assume c in the carrier of A & d in the carrier of A;
then reconsider f = c, g = d as Homeomorphism of T by A5;
thus (the multF of A).(c,d) = g * f by A5
.= (the multF of B).(c,d) by A6;
end;
A9: for x being object holds x in the carrier of A iff X[x] by A5;
the carrier of A = the carrier of B from XBOOLE_0:sch 2(A9,A7);
hence thesis by A8,BINOP_1:1;
end;
end;
registration
let T be TopStruct;
cluster HomeoGroup T -> non empty;
coherence
proof
id T is Homeomorphism of T;
hence the carrier of HomeoGroup T is non empty by Def5;
end;
end;
theorem
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 by Def5;
registration
let T be TopStruct;
cluster HomeoGroup T -> Group-like associative;
coherence
proof
set G = HomeoGroup T, o = the multF of G;
thus G is Group-like
proof
reconsider e = id T as Element of G by Def5;
take e;
let h be Element of G;
reconsider h1 = h, e1 = e as Homeomorphism of T by Def5;
thus h * e = e1 * h1 by Def5
.= h by FUNCT_2:17;
thus e * h = h1 * e1 by Def5
.= h by FUNCT_2:17;
reconsider h1 = h as Homeomorphism of T by Def5;
A1: dom h1 = [#]T by TOPS_2:def 5;
h1/" is Homeomorphism of T by Th29;
then reconsider g = h1/" as Element of G by Def5;
reconsider g1 = g as Homeomorphism of T by Def5;
take g;
A2: rng h1 = [#]T by TOPS_2:def 5;
thus h * g = g1 * h1 by Def5
.= e by A1,A2,TOPS_2:52;
thus g * h = h1 * g1 by Def5
.= e by A2,TOPS_2:52;
end;
let x, y, z be Element of G;
reconsider f = x, g = y as Homeomorphism of T by Def5;
reconsider p = g*f, r = z as Homeomorphism of T by Def5,Th30;
reconsider a = r*g as Homeomorphism of T by Th30;
thus (x*y)*z = o.(g*f,z) by Def5
.= r * p by Def5
.= (r * g) * f by RELAT_1:36
.= o.(f,a) by Def5
.= x*(y*z) by Def5;
end;
end;
theorem Th32:
id T = 1_HomeoGroup T
proof
set G = HomeoGroup T;
reconsider e = id T as Element of G by Def5;
now
let h be Element of G;
reconsider h1 = h as Homeomorphism of T by Def5;
thus h * e = id T * h1 by Def5
.= h by FUNCT_2:17;
thus e * h = h1 * id T by Def5
.= h by FUNCT_2:17;
end;
hence thesis by GROUP_1:4;
end;
theorem
for f being Homeomorphism of T for a being Element of HomeoGroup T st
f = a holds a" = f/"
proof
let f be Homeomorphism of T;
set G = HomeoGroup T;
A1: dom f = [#]T by TOPS_2:def 5;
A2: f/" is Homeomorphism of T by Def4;
then reconsider g = f/" as Element of G by Def5;
A3: rng f = [#]T by TOPS_2:def 5;
let a be Element of HomeoGroup T such that
A4: f = a;
A5: g * a = f * (f/") by A4,A2,Def5
.= id T by A3,TOPS_2:52
.= 1_G by Th32;
a * g = f/" * f by A4,A2,Def5
.= id T by A1,A3,TOPS_2:52
.= 1_G by Th32;
hence thesis by A5,GROUP_1:5;
end;
definition
let T be TopStruct;
attr T is homogeneous means
:Def6:
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;
coherence
proof
let T be 1-element TopStruct;
let p, q be Point of T;
take id T;
thus (id T).p = q by STRUCT_0:def 10;
end;
end;
theorem
for T being homogeneous non empty TopSpace st ex p being Point of T st
{p} is closed holds T is T_1
proof
let T be homogeneous non empty TopSpace;
given p being Point of T such that
A1: {p} is closed;
now
let q be Point of T;
consider f being Homeomorphism of T such that
A2: f.p = q by Def6;
dom f = the carrier of T by FUNCT_2:def 1;
then Im(f,p) = {f.p} by FUNCT_1:59;
hence {q} is closed by A1,A2,TOPS_2:58;
end;
hence thesis by URYSOHN1:19;
end;
theorem Th35:
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
proof
let T be homogeneous non empty TopSpace;
given p being Point of T such that
A1: 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;
A2: [#]T <> {};
now
let A be open Subset of T, q be Point of T such that
A3: q in A;
consider f being Homeomorphism of T such that
A4: f.p = q by Def6;
A5: f"A is open by A2,TOPS_2:43;
reconsider g = f as Function;
A6: dom f = the carrier of T by FUNCT_2:def 1;
A7: rng f = [#]T by TOPS_2:def 5;
then g".q = f".q & g.(g".q) in A by A3,FUNCT_1:32;
then
A8: g".q in g"A by A6,FUNCT_1:def 7;
p = g".q by A4,A6,FUNCT_1:32;
then consider B being Subset of T such that
A9: p in B and
A10: B is open and
A11: Cl B c= f"A by A1,A8,A5;
reconsider fB = f.:B as open Subset of T by A10,Th24;
take fB;
thus q in fB by A4,A6,A9,FUNCT_1:def 6;
A12: f.:Cl B = Cl fB by TOPS_2:60;
f.:Cl B c= f.:(f"A) by A11,RELAT_1:123;
hence Cl fB c= A by A7,A12,FUNCT_1:77;
end;
hence thesis by URYSOHN1:21;
end;
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;
coherence;
end;
registration
let x be set, R be BinOp of {x}, T be Subset-Family of {x};
cluster TopGrStr (#{x}, R, T#) -> trivial;
coherence;
end;
registration
cluster -> Group-like associative commutative for 1-element multMagma;
coherence
proof
let H be 1-element multMagma;
hereby
set e = the Element of H;
take e;
let h be Element of H;
thus h * e = h & e * h = h by STRUCT_0:def 10;
take g = e;
thus h * g = e & g * h = e by STRUCT_0:def 10;
end;
thus for x, y, z being Element of H holds x*y*z = x*(y*z)
by STRUCT_0:def 10;
let x, y be Element of H;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
let a be set;
cluster 1TopSp {a} -> trivial;
coherence;
end;
registration
cluster strict non empty for TopGrStr;
existence
proof
set R = the BinOp of {{}},T = the Subset-Family of {{}};
take TopGrStr (#{{}},R,T#);
thus thesis;
end;
end;
registration
cluster strict TopSpace-like 1-element for TopGrStr;
existence
proof
set R = the BinOp of {{}};
take TopGrStr (#{{}}, R, bool {{}}#);
the carrier of 1TopSp {{}} is 1-element;
hence thesis by TEX_2:7;
end;
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
:Def7:
inverse_op G is continuous;
end;
definition
let G be TopSpace-like TopGrStr;
attr G is BinContinuous means
:Def8:
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;
existence
proof
set R = the BinOp of {{}};
1TopSp {{}} is 1-element;
then reconsider
T = TopGrStr (#{{}}, R, bool {{}}#) as strict TopSpace-like
1-element TopGrStr by TEX_2:7;
take T;
thus T is strict commutative;
hereby
set f = inverse_op T;
thus f is continuous
proof
let P1 be Subset of T such that
P1 is closed;
per cases by ZFMISC_1:33;
suppose
f"P1 = {};
hence thesis;
end;
suppose
f"P1 = {{}};
then f"P1 = [#]T;
hence thesis;
end;
end;
end;
let f be Function of [:T,T:], T such that
f = the multF of T;
A1: the carrier of [:T,T:] = [:{{}},{{}}:] by BORSUK_1:def 2
.= {[{},{}]} by ZFMISC_1:29;
let P1 be Subset of T such that
P1 is closed;
per cases by A1,ZFMISC_1:33;
suppose
f"P1 = {};
hence thesis;
end;
suppose
f"P1 = {[{},{}]};
then f"P1 = [#][:T,T:] by A1;
hence thesis;
end;
end;
end;
definition
mode TopGroup is TopSpace-like Group-like associative non empty TopGrStr;
end;
definition
mode TopologicalGroup is UnContinuous BinContinuous TopGroup;
end;
theorem Th36:
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
proof
let T be BinContinuous non empty TopSpace-like TopGrStr, a, b be Element
of T, W be a_neighborhood of a*b;
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by
BORSUK_1:def 2;
then reconsider f = the multF of T as Function of [:T,T:], T;
f is continuous by Def8;
then consider H being a_neighborhood of [a,b] such that
A1: f.:H c= W by BORSUK_1:def 1;
consider F being Subset-Family of [:T,T:] such that
A2: Int H = union F and
A3: for e being set st e in F ex X1, Y1 being Subset of T st e = [:X1,Y1
:] & X1 is open & Y1 is open by BORSUK_1:5;
[a,b] in Int H by CONNSP_2:def 1;
then consider M being set such that
A4: [a,b] in M and
A5: M in F by A2,TARSKI:def 4;
consider A, B being Subset of T such that
A6: M = [:A,B:] and
A7: A is open and
A8: B is open by A3,A5;
a in A by A4,A6,ZFMISC_1:87;
then
A9: a in Int A by A7,TOPS_1:23;
b in B by A4,A6,ZFMISC_1:87;
then b in Int B by A8,TOPS_1:23;
then reconsider B as open a_neighborhood of b by A8,CONNSP_2:def 1;
reconsider A as open a_neighborhood of a by A7,A9,CONNSP_2:def 1;
take A, B;
let x be object;
assume x in A*B;
then consider g, h being Element of T such that
A10: x = g*h and
A11: g in A & h in B;
A12: Int H c= H by TOPS_1:16;
[g,h] in M by A6,A11,ZFMISC_1:87;
then [g,h] in Int H by A2,A5,TARSKI:def 4;
then x in f.:H by A10,A12,FUNCT_2:35;
hence thesis by A1;
end;
theorem Th37:
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
proof
let T be TopSpace-like non empty TopGrStr such that
A1: 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;
let f be Function of [:T,T:], T such that
A2: f = the multF of T;
for W being Point of [:T,T:], G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
let W be Point of [:T,T:], G be a_neighborhood of f.W;
consider a, b being Point of T such that
A3: W = [a,b] by BORSUK_1:10;
f.W = a*b by A2,A3;
then consider
A being a_neighborhood of a, B being a_neighborhood of b such
that
A4: A*B c= G by A1;
reconsider H = [:A,B:] as a_neighborhood of W by A3;
take H;
thus thesis by A2,A4,Th14;
end;
hence thesis by BORSUK_1:def 1;
end;
theorem Th38:
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
proof
let T be UnContinuous TopGroup, a be Element of T, W be a_neighborhood of a";
reconsider f = inverse_op T as Function of T, T;
f.a = a" & f is continuous by Def7,GROUP_1:def 6;
then consider H being a_neighborhood of a such that
A1: f.:H c= W by BORSUK_1:def 1;
a in Int Int H by CONNSP_2:def 1;
then reconsider A = Int H as open a_neighborhood of a by CONNSP_2:def 1;
take A;
let x be object;
assume x in A";
then consider g being Element of T such that
A2: x = g" and
A3: g in A;
Int H c= H & f.g = g" by GROUP_1:def 6,TOPS_1:16;
then g" in f.:H by A3,FUNCT_2:35;
hence thesis by A1,A2;
end;
theorem Th39:
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
proof
let T be TopGroup such that
A1: for a being Element of T, W being a_neighborhood of a" ex A being
a_neighborhood of a st A" c= W;
set f = inverse_op T;
for W being Point of T, G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
let a be Point of T, G be a_neighborhood of f.a;
f.a = a" by GROUP_1:def 6;
then consider A being a_neighborhood of a such that
A2: A" c= G by A1;
take A;
thus thesis by A2,Th9;
end;
hence f is continuous by BORSUK_1:def 1;
end;
theorem Th40:
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
proof
let T be TopologicalGroup, a, b be Element of T, W be a_neighborhood of a*(b
");
consider A being open a_neighborhood of a, B being open a_neighborhood of b"
such that
A1: A*B c= W by Th36;
consider C being open a_neighborhood of b such that
A2: C" c= B by Th38;
take A, C;
let x be object;
assume x in A*(C");
then consider g, h being Element of T such that
A3: x = g*h and
A4: g in A and
A5: h in C";
consider k being Element of T such that
A6: h = k" and
k in C by A5;
g*(k") in A*B by A2,A4,A5,A6;
hence thesis by A1,A3,A6;
end;
theorem
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
proof
let T be TopGroup such that
A1: 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;
A2: for a being Element of T, W being a_neighborhood of a" ex A being
a_neighborhood of a st A" c= W
proof
let a be Element of T, W be a_neighborhood of a";
W is a_neighborhood of 1_T*(a") by GROUP_1:def 4;
then consider
A being a_neighborhood of 1_T, B being a_neighborhood of a such
that
A3: A*(B") c= W by A1;
take B;
let x be object;
assume
A4: x in B";
then consider g being Element of T such that
A5: x = g" and
g in B;
1_T in A by CONNSP_2:4;
then 1_T * (g") in A*(B") by A4,A5;
then g" in A*(B") by GROUP_1:def 4;
hence thesis by A3,A5;
end;
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
proof
let a, b be Element of T, W be a_neighborhood of a*b;
W is a_neighborhood of a*(b"");
then consider
A being a_neighborhood of a, B being a_neighborhood of b" such
that
A6: A*(B") c= W by A1;
consider B1 being a_neighborhood of b such that
A7: B1" c= B by A2;
take A, B1;
let x be object;
assume x in A * B1;
then consider g, h being Element of T such that
A8: x = g * h & g in A and
A9: h in B1;
h" in B1" by A9;
then h in B" by A7,Th7;
then x in A*(B") by A8;
hence thesis by A6;
end;
hence thesis by A2,Th37,Th39;
end;
registration
let G be BinContinuous non empty TopSpace-like TopGrStr, a be Element of G;
cluster a* -> continuous;
coherence
proof
set f = a*;
for w being Point of G, A being a_neighborhood of f.w ex W being
a_neighborhood of w st f.:W c= A
proof
let w be Point of G, A be a_neighborhood of f.w;
f.w = a * w by Def1;
then consider
B being open a_neighborhood of a, W being open a_neighborhood
of w such that
A1: B*W c= A by Th36;
take W;
let k be object;
assume k in f.:W;
then k in a * W by Th15;
then
A2: ex h being Element of G st k = a * h & h in W by GROUP_2:27;
a in B by CONNSP_2:4;
then k in B * W by A2;
hence thesis by A1;
end;
hence thesis by BORSUK_1:def 1;
end;
cluster *a -> continuous;
coherence
proof
set f = *a;
for w being Point of G, A being a_neighborhood of f.w ex W being
a_neighborhood of w st f.:W c= A
proof
let w be Point of G, A be a_neighborhood of f.w;
f.w = w * a by Def2;
then consider
W being open a_neighborhood of w, B being open a_neighborhood
of a such that
A3: W*B c= A by Th36;
take W;
let k be object;
assume k in f.:W;
then k in W * a by Th16;
then
A4: ex h being Element of G st k = h * a & h in W by GROUP_2:28;
a in B by CONNSP_2:4;
then k in W * B by A4;
hence thesis by A3;
end;
hence thesis by BORSUK_1:def 1;
end;
end;
theorem Th42:
for G being BinContinuous TopGroup, a being Element of G holds a
* is Homeomorphism of G
proof
let G be BinContinuous TopGroup, a be Element of G;
set f = a*;
thus dom f = [#]G & rng f = [#]G & f is one-to-one by FUNCT_2:def 1,def 3;
thus f is continuous;
f/" = (a"*) by Th17;
hence thesis;
end;
theorem Th43:
for G being BinContinuous TopGroup, a being Element of G holds *
a is Homeomorphism of G
proof
let G be BinContinuous TopGroup, a be Element of G;
set f = *a;
thus dom f = [#]G & rng f = [#]G & f is one-to-one by FUNCT_2:def 1,def 3;
thus f is continuous;
f/" = *(a") by Th18;
hence thesis;
end;
definition
let G be BinContinuous TopGroup, a be Element of G;
redefine func a* -> Homeomorphism of G; :: redefines * (TOPGRP_1, definition)
coherence by Th42;
redefine func *a -> Homeomorphism of G; :: redefines * (TOPGRP_1, definition)
coherence by Th43;
end;
theorem Th44:
for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G
proof
let G be UnContinuous TopGroup;
set f = inverse_op G;
thus
dom f = [#]G & rng f = [#]G & f is one-to-one by FUNCT_2:def 1,def 3;
thus f is continuous by Def7;
f = (f qua Function)" by Th13
.= f/" by TOPS_2:def 4;
hence thesis by Def7;
end;
definition
let G be UnContinuous TopGroup;
redefine func inverse_op G -> Homeomorphism of G; :: redefines inverse_op (GROUP_1, definition)
coherence by Th44;
end;
registration
cluster BinContinuous -> homogeneous for TopGroup;
coherence
proof
let T be TopGroup;
assume T is BinContinuous;
then reconsider G = T as BinContinuous TopGroup;
G is homogeneous
proof
let p, q be Point of G;
take *(p"*q);
thus (*(p"*q)).p = p*(p"*q) by Def2
.= p*p"*q by GROUP_1:def 3
.= 1_G*q by GROUP_1:def 5
.= q by GROUP_1:def 4;
end;
hence thesis;
end;
end;
theorem Th45:
for G being BinContinuous TopGroup, F being closed Subset of G,
a being Element of G holds F * a is closed
proof
let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G;
F * a = (*a).:F by Th16;
hence thesis by TOPS_2:58;
end;
theorem Th46:
for G being BinContinuous TopGroup, F being closed Subset of G,
a being Element of G holds a * F is closed
proof
let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G;
a * F = (a*).:F by Th15;
hence thesis by TOPS_2:58;
end;
registration
let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G;
cluster F * a -> closed;
coherence by Th45;
cluster a * F -> closed;
coherence by Th46;
end;
theorem Th47:
for G being UnContinuous TopGroup, F being closed Subset of G
holds F" is closed
proof
let G be UnContinuous TopGroup, F be closed Subset of G;
F" = (inverse_op G).:F by Th9;
hence thesis by TOPS_2:58;
end;
registration
let G be UnContinuous TopGroup, F be closed Subset of G;
cluster F" -> closed;
coherence by Th47;
end;
theorem Th48:
for G being BinContinuous TopGroup, O being open Subset of G, a
being Element of G holds O * a is open
proof
let G be BinContinuous TopGroup, O be open Subset of G, a be Element of G;
O * a = (*a).:O by Th16;
hence thesis by Th24;
end;
theorem Th49:
for G being BinContinuous TopGroup, O being open Subset of G, a
being Element of G holds a * O is open
proof
let G be BinContinuous TopGroup, O be open Subset of G, a be Element of G;
a * O = (a*).:O by Th15;
hence thesis by Th24;
end;
registration
let G be BinContinuous TopGroup, A be open Subset of G, a be Element of G;
cluster A * a -> open;
coherence by Th48;
cluster a * A -> open;
coherence by Th49;
end;
theorem Th50:
for G being UnContinuous TopGroup, O being open Subset of G holds O" is open
proof
let G be UnContinuous TopGroup, O be open Subset of G;
O" = (inverse_op G).:O by Th9;
hence thesis by Th24;
end;
registration
let G be UnContinuous TopGroup, A be open Subset of G;
cluster A" -> open;
coherence by Th50;
end;
theorem Th51:
for G being BinContinuous TopGroup, A, O being Subset of G st O
is open holds O * A is open
proof
let G be BinContinuous TopGroup, A, O be Subset of G such that
A1: O is open;
Int (O * A) = O * A
proof
thus Int (O * A) c= O * A by TOPS_1:16;
let x be object;
assume x in O * A;
then consider o, a being Element of G such that
A2: x = o * a & o in O and
A3: a in A;
set Q = O * a;
A4: Q c= O * A
proof
let q be object;
assume q in Q;
then ex h being Element of G st q = h * a & h in O by GROUP_2:28;
hence thesis by A3;
end;
x in Q by A2,GROUP_2:28;
hence thesis by A1,A4,TOPS_1:22;
end;
hence thesis;
end;
theorem Th52:
for G being BinContinuous TopGroup, A, O being Subset of G st O
is open holds A * O is open
proof
let G be BinContinuous TopGroup, A, O be Subset of G such that
A1: O is open;
Int (A * O) = A * O
proof
thus Int (A * O) c= A * O by TOPS_1:16;
let x be object;
assume x in A * O;
then consider a, o being Element of G such that
A2: x = a * o and
A3: a in A and
A4: o in O;
set Q = a * O;
A5: Q c= A * O
proof
let q be object;
assume q in Q;
then ex h being Element of G st q = a * h & h in O by GROUP_2:27;
hence thesis by A3;
end;
x in Q by A2,A4,GROUP_2:27;
hence thesis by A1,A5,TOPS_1:22;
end;
hence thesis;
end;
registration
let G be BinContinuous TopGroup, A be open Subset of G, B be Subset of G;
cluster A * B -> open;
coherence by Th51;
cluster B * A -> open;
coherence by Th52;
end;
theorem Th53:
for G being UnContinuous TopGroup, a being Point of G, A being
a_neighborhood of a holds A" is a_neighborhood of a"
proof
let G be UnContinuous TopGroup, a be Point of G, A be a_neighborhood of a;
a in Int A by CONNSP_2:def 1;
then consider Q being Subset of G such that
A1: Q is open and
A2: Q c= A & a in Q by TOPS_1:22;
Q" c= A" & a" in Q" by A2,Th8;
hence a" in Int (A") by A1,TOPS_1:22;
end;
theorem Th54:
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
proof
let G be TopologicalGroup, a be Point of G, A be a_neighborhood of a*a";
consider X, Y being open a_neighborhood of a such that
A1: X*Y" c= A by Th40;
reconsider B = X /\ Y as open a_neighborhood of a by CONNSP_2:2;
take B;
let x be object;
assume x in B*B";
then consider g, h being Point of G such that
A2: x = g*h and
A3: g in B and
A4: h in B";
h" in B by A4,Th7;
then h" in Y by XBOOLE_0:def 4;
then
A5: h in Y" by Th7;
g in X by A3,XBOOLE_0:def 4;
then x in X*Y" by A2,A5;
hence thesis by A1;
end;
theorem Th55:
for G being UnContinuous TopGroup, A being dense Subset of G
holds A" is dense
proof
let G be UnContinuous TopGroup, A be dense Subset of G;
(inverse_op G)"A = A" by Th10;
hence thesis by Th28;
end;
registration
let G be UnContinuous TopGroup, A be dense Subset of G;
cluster A" -> dense;
coherence by Th55;
end;
theorem Th56:
for G being BinContinuous TopGroup, A being dense Subset of G, a
being Point of G holds a*A is dense
proof
let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;
(a*).:A = a*A by Th15;
hence thesis by Th27;
end;
theorem Th57:
for G being BinContinuous TopGroup, A being dense Subset of G, a
being Point of G holds A*a is dense
proof
let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;
(*a).:A = A*a by Th16;
hence thesis by Th27;
end;
registration
let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;
cluster A * a -> dense;
coherence by Th57;
cluster a * A -> dense;
coherence by Th56;
end;
theorem
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
proof
let G be TopologicalGroup, B be Basis of 1_G, M be dense Subset of G;
set Z = { V * x where V is Subset of G, x is Point of G: V in B & x in M };
A1: Z c= the topology of G
proof
let a be object;
assume a in Z;
then consider V being Subset of G, x being Point of G such that
A2: a = V*x and
A3: V in B and
x in M;
reconsider V as Subset of G;
V is open by A3,YELLOW_8:12;
hence thesis by A2,PRE_TOPC:def 2;
end;
A4: for W being Subset of G st W is open for a being Point of G st a in W ex
V being Subset of G st V in Z & a in V & V c= W
proof
A5: 1_G*(1_G)" = 1_G*1_G by GROUP_1:8
.= 1_G by GROUP_1:def 4;
let W be Subset of G such that
A6: W is open;
let a be Point of G such that
A7: a in W;
1_G = a*a" by GROUP_1:def 5;
then 1_G in W*a" by A7,GROUP_2:28;
then W*a" is a_neighborhood of 1_G*(1_G)" by A6,A5,CONNSP_2:3;
then consider V being open a_neighborhood of 1_G such that
A8: V*V" c= W*a" by Th54;
consider E being Subset of G such that
A9: E in B and
A10: E c= V by CONNSP_2:4,YELLOW_8:13;
E is open & E <> {} by A9,YELLOW_8:12;
then (a*M") meets E by TOPS_1:45;
then consider d being object such that
A11: d in (a*M") /\ E by XBOOLE_0:4;
reconsider d as Point of G by A11;
take I = E*(d"*a);
d in a*M" by A11,XBOOLE_0:def 4;
then consider m being Point of G such that
A12: d = a*m and
A13: m in M" by GROUP_2:27;
d"*a = d"*a*1_G by GROUP_1:def 4
.= d"*a*(m*m") by GROUP_1:def 5
.= d"*a*m*m" by GROUP_1:def 3
.= d"*d*m" by A12,GROUP_1:def 3
.= 1_G*m" by GROUP_1:def 5
.= m" by GROUP_1:def 4;
then d"*a in M by A13,Th7;
hence I in Z by A9;
A14: 1_G*a = a by GROUP_1:def 4;
A15: d in E by A11,XBOOLE_0:def 4;
E*d" c= V*V"
proof
let q be object;
assume q in E*d";
then
A16: ex v being Point of G st q = v*d" & v in E by GROUP_2:28;
d" in V" by A10,A15;
hence thesis by A10,A16;
end;
then E*d" c= W*a" by A8;
then
A17: E*d"*a c= W*a"*a by Th5;
d*d" = 1_G by GROUP_1:def 5;
then 1_G in E*d" by A15,GROUP_2:28;
then a in E*d"*a by A14,GROUP_2:28;
hence a in I by GROUP_2:34;
W*a"*a = W*(a"*a) by GROUP_2:34
.= W*1_G by GROUP_1:def 5
.= W by GROUP_2:37;
hence thesis by A17,GROUP_2:34;
end;
Z c= bool the carrier of G
proof
let a be object;
assume a in Z;
then
ex V being Subset of G, x being Point of G st a = V*x & V in B & x in M;
hence thesis;
end;
hence thesis by A1,A4,YELLOW_9:32;
end;
theorem Th59:
for G being TopologicalGroup holds G is regular
proof
let G be TopologicalGroup;
ex p being Point of G st for A being Subset of G st A is open & p in A
holds ex B being Subset of G st p in B & B is open & Cl B c= A
proof
set e = 1_G;
take e;
let A be Subset of G;
assume A is open & e in A;
then e in Int A by TOPS_1:23;
then
A1: A is a_neighborhood of e by CONNSP_2:def 1;
e = e*e" by GROUP_1:def 5;
then consider
C being open a_neighborhood of e, B being open a_neighborhood of
e" such that
A2: C*B c= A by A1,Th36;
e"" = e;
then B" is a_neighborhood of e by Th53;
then reconsider W = C /\ (B") as a_neighborhood of e by CONNSP_2:2;
W c= B" by XBOOLE_1:17;
then W" c= B"" by Th8;
then C*W" c= C*B by Th4;
then
A3: C*W" c= A by A2;
take W;
Int W = W by TOPS_1:23;
hence
A4: e in W & W is open by CONNSP_2:def 1;
let p be object;
assume
A5: p in Cl W;
then reconsider r = p as Point of G;
r = r*e by GROUP_1:def 4;
then p in r*W by A4,GROUP_2:27;
then (r*W) meets W by A5,PRE_TOPC:def 7;
then consider a being object such that
A6: a in (r*W) /\ W by XBOOLE_0:4;
A7: a in W by A6,XBOOLE_0:def 4;
A8: a in r*W by A6,XBOOLE_0:def 4;
reconsider a as Point of G by A6;
consider b being Element of G such that
A9: a = r * b and
A10: b in W by A8,GROUP_2:27;
A11: W c= C & b" in W" by A10,XBOOLE_1:17;
r = r * e by GROUP_1:def 4
.= r * (b * b") by GROUP_1:def 5
.= a * (b") by A9,GROUP_1:def 3;
then p in C * W" by A7,A11;
hence thesis by A3;
end;
hence thesis by Th35;
end;
registration
cluster -> regular for TopologicalGroup;
coherence by Th59;
end;
theorem
for T being TopStruct, f be Function of T,T st T is empty holds f is
being_homeomorphism by Lm2;