:: TOPGRP_1 semantic presentation
begin
registration
let X be set ;
cluster Relation-like X -defined X -valued Function-like one-to-one V14(X) quasi_total onto for Element of bool [:X,X:];
existence
ex b1 being Function of X,X st
( b1 is one-to-one & b1 is onto )
proof
take id X ; ::_thesis: ( id X is one-to-one & id X is onto )
thus id X is one-to-one ; ::_thesis: id X is onto
thus rng (id X) = X by RELAT_1:45; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;
theorem :: TOPGRP_1:1
for S being 1-sorted holds rng (id S) = [#] S by RELAT_1:45;
registration
let R be 1-sorted ;
cluster(id R) /" -> one-to-one ;
coherence
(id R) /" is one-to-one
proof
rng (id R) = [#] R by RELAT_1:45;
hence (id R) /" is one-to-one by TOPS_2:50; ::_thesis: verum
end;
end;
theorem Th2: :: TOPGRP_1:2
for R being 1-sorted holds (id R) /" = id R
proof
let R be 1-sorted ; ::_thesis: (id R) /" = id R
rng (id R) = [#] R by RELAT_1:45;
then id R is onto by FUNCT_2:def_3;
hence (id R) /" = (id the carrier of R) " by TOPS_2:def_4
.= id R by FUNCT_1:45 ;
::_thesis: verum
end;
theorem :: TOPGRP_1:3
for R being 1-sorted
for X being Subset of R holds (id R) " X = X
proof
let R be 1-sorted ; ::_thesis: for X being Subset of R holds (id R) " X = X
let X be Subset of R; ::_thesis: (id R) " X = X
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 (id R) " X = X by A1, FUNCT_1:92; ::_thesis: verum
end;
begin
theorem Th4: :: TOPGRP_1:4
for H being non empty multMagma
for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1
proof
let H be non empty multMagma ; ::_thesis: for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1
let P, P1, Q, Q1 be Subset of H; ::_thesis: ( P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1 )
assume A1: ( P c= P1 & Q c= Q1 ) ; ::_thesis: P * Q c= P1 * Q1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P * Q or x in P1 * Q1 )
assume x in P * Q ; ::_thesis: x in P1 * Q1
then ex g, t being Element of H st
( x = g * t & g in P & t in Q ) ;
hence x in P1 * Q1 by A1; ::_thesis: verum
end;
theorem Th5: :: TOPGRP_1:5
for H being non empty multMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
P * h c= Q * h
proof
let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H
for h being Element of H st P c= Q holds
P * h c= Q * h
let P, Q be Subset of H; ::_thesis: for h being Element of H st P c= Q holds
P * h c= Q * h
let h be Element of H; ::_thesis: ( P c= Q implies P * h c= Q * h )
assume A1: P c= Q ; ::_thesis: P * h c= Q * h
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P * h or x in Q * h )
assume x in P * h ; ::_thesis: x in Q * h
then ex g being Element of H st
( x = g * h & g in P ) by GROUP_2:28;
hence x in Q * h by A1, GROUP_2:28; ::_thesis: verum
end;
theorem :: TOPGRP_1:6
for H being non empty multMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
h * P c= h * Q
proof
let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H
for h being Element of H st P c= Q holds
h * P c= h * Q
let P, Q be Subset of H; ::_thesis: for h being Element of H st P c= Q holds
h * P c= h * Q
let h be Element of H; ::_thesis: ( P c= Q implies h * P c= h * Q )
assume A1: P c= Q ; ::_thesis: h * P c= h * Q
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h * P or x in h * Q )
assume x in h * P ; ::_thesis: x in h * Q
then ex g being Element of H st
( x = h * g & g in P ) by GROUP_2:27;
hence x in h * Q by A1, GROUP_2:27; ::_thesis: verum
end;
theorem Th7: :: TOPGRP_1:7
for G being Group
for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )
proof
let G be Group; ::_thesis: for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )
let A be Subset of G; ::_thesis: for a being Element of G holds
( a in A " iff a " in A )
let a be Element of G; ::_thesis: ( a in A " iff a " in A )
( (a ") " = a & (A ") " = A ) ;
hence ( a in A " iff a " in A ) ; ::_thesis: verum
end;
Lm1: for G being Group
for A, B being Subset of G st A c= B holds
A " c= B "
proof
let G be Group; ::_thesis: for A, B being Subset of G st A c= B holds
A " c= B "
let A, B be Subset of G; ::_thesis: ( A c= B implies A " c= B " )
assume A1: A c= B ; ::_thesis: A " c= B "
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A " or a in B " )
assume a in A " ; ::_thesis: a in B "
then ex g being Element of G st
( a = g " & g in A ) ;
hence a in B " by A1; ::_thesis: verum
end;
theorem :: TOPGRP_1:8
canceled;
theorem Th9: :: TOPGRP_1:9
for G being Group
for A, B being Subset of G holds
( A c= B iff A " c= B " )
proof
let G be Group; ::_thesis: for A, B being Subset of G holds
( A c= B iff A " c= B " )
let A, B be Subset of G; ::_thesis: ( A c= B iff A " c= B " )
( (A ") " = A & (B ") " = B ) ;
hence ( A c= B iff A " c= B " ) by Lm1; ::_thesis: verum
end;
theorem Th10: :: TOPGRP_1:10
for G being Group
for A being Subset of G holds (inverse_op G) .: A = A "
proof
let G be Group; ::_thesis: for A being Subset of G holds (inverse_op G) .: A = A "
let A be Subset of G; ::_thesis: (inverse_op G) .: A = A "
set f = inverse_op G;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A " c= (inverse_op G) .: A
let y be set ; ::_thesis: ( y in (inverse_op G) .: A implies y in A " )
assume y in (inverse_op G) .: A ; ::_thesis: y in A "
then consider x being set such that
A1: x in the carrier of G and
A2: x in A and
A3: y = (inverse_op G) . x by FUNCT_2:64;
reconsider x = x as Element of G by A1;
y = x " by A3, GROUP_1:def_6;
hence y in A " by A2; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A " or y in (inverse_op G) .: A )
assume y in A " ; ::_thesis: y in (inverse_op G) .: A
then consider g being Element of G such that
A4: ( y = g " & g in A ) ;
(inverse_op G) . g = g " by GROUP_1:def_6;
hence y in (inverse_op G) .: A by A4, FUNCT_2:35; ::_thesis: verum
end;
theorem Th11: :: TOPGRP_1:11
for G being Group
for A being Subset of G holds (inverse_op G) " A = A "
proof
let G be Group; ::_thesis: for A being Subset of G holds (inverse_op G) " A = A "
let A be Subset of G; ::_thesis: (inverse_op G) " A = A "
set f = inverse_op G;
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A " c= (inverse_op G) " A
let x be set ; ::_thesis: ( x in (inverse_op G) " A implies x in A " )
assume A2: x in (inverse_op G) " A ; ::_thesis: x in A "
then reconsider g = x as Element of G ;
(inverse_op G) . x in A by A2, FUNCT_1:def_7;
then ((inverse_op G) . g) " in A " ;
then (g ") " in A " by GROUP_1:def_6;
hence x in A " ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in (inverse_op G) " A )
assume x in A " ; ::_thesis: x in (inverse_op G) " A
then consider g being Element of G such that
A3: ( x = g " & g in A ) ;
(inverse_op G) . (g ") = (g ") " by GROUP_1:def_6
.= g ;
hence x in (inverse_op G) " A by A1, A3, FUNCT_1:def_7; ::_thesis: verum
end;
theorem Th12: :: TOPGRP_1:12
for G being Group holds inverse_op G is one-to-one
proof
let G be Group; ::_thesis: inverse_op G is one-to-one
set f = inverse_op G;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (inverse_op G) or not x2 in dom (inverse_op G) or not (inverse_op G) . x1 = (inverse_op G) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (inverse_op G) & x2 in dom (inverse_op G) ) and
A2: (inverse_op G) . x1 = (inverse_op G) . x2 ; ::_thesis: x1 = x2
reconsider a = x1, b = x2 as Element of G by A1;
( (inverse_op G) . a = a " & (inverse_op G) . b = b " ) by GROUP_1:def_6;
hence x1 = x2 by A2, GROUP_1:9; ::_thesis: verum
end;
theorem Th13: :: TOPGRP_1:13
for G being Group holds rng (inverse_op G) = the carrier of G
proof
let G be Group; ::_thesis: rng (inverse_op G) = the carrier of G
set f = inverse_op G;
thus rng (inverse_op G) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (inverse_op G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in rng (inverse_op G) )
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1;
assume x in the carrier of G ; ::_thesis: x in rng (inverse_op G)
then reconsider a = x as Element of G ;
(inverse_op G) . (a ") = (a ") " by GROUP_1:def_6
.= a ;
hence x in rng (inverse_op G) by A1, FUNCT_1:def_3; ::_thesis: verum
end;
registration
let G be Group;
cluster inverse_op G -> one-to-one onto ;
coherence
( inverse_op G is one-to-one & inverse_op G is onto )
proof
thus inverse_op G is one-to-one by Th12; ::_thesis: inverse_op G is onto
thus rng (inverse_op G) = the carrier of G by Th13; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;
theorem Th14: :: TOPGRP_1:14
for G being Group holds (inverse_op G) " = inverse_op G
proof
let G be Group; ::_thesis: (inverse_op G) " = inverse_op G
set f = inverse_op G;
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(inverse_op_G)_holds_
(inverse_op_G)_._x_=_((inverse_op_G)_")_._x
let x be set ; ::_thesis: ( x in dom (inverse_op G) implies (inverse_op G) . x = ((inverse_op G) ") . x )
assume x in dom (inverse_op G) ; ::_thesis: (inverse_op G) . x = ((inverse_op G) ") . x
then reconsider g = x as Element of G ;
A3: (inverse_op G) . (g ") = (g ") " by GROUP_1:def_6
.= g ;
thus (inverse_op G) . x = g " by GROUP_1:def_6
.= ((inverse_op G) ") . x by A1, A3, FUNCT_1:32 ; ::_thesis: verum
end;
dom ((inverse_op G) ") = the carrier of G by FUNCT_2:def_1;
hence (inverse_op G) " = inverse_op G by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th15: :: TOPGRP_1:15
for H being non empty multMagma
for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q
proof
let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q
let P, Q be Subset of H; ::_thesis: the multF of H .: [:P,Q:] = P * Q
set f = the multF of H;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P * Q c= the multF of H .: [:P,Q:]
let y be set ; ::_thesis: ( y in the multF of H .: [:P,Q:] implies y in P * Q )
assume y in the multF of H .: [:P,Q:] ; ::_thesis: y in P * Q
then consider x being set such that
x in [: the carrier of H, the carrier of H:] and
A1: x in [:P,Q:] and
A2: y = the multF of H . x by FUNCT_2:64;
consider a, b being set such that
A3: ( a in P & b in Q ) and
A4: x = [a,b] by A1, ZFMISC_1:def_2;
reconsider a = a, b = b as Element of H by A3;
y = a * b by A2, A4;
hence y in P * Q by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P * Q or y in the multF of H .: [:P,Q:] )
assume y in P * Q ; ::_thesis: y in the multF of H .: [: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 y in the multF of H .: [:P,Q:] by A5, FUNCT_2:35; ::_thesis: verum
end;
definition
let G be non empty multMagma ;
let a be Element of G;
funca * -> Function of G,G means :Def1: :: TOPGRP_1:def 1
for x being Element of G holds it . x = a * x;
existence
ex b1 being Function of G,G st
for x being Element of G holds b1 . x = a * x
proof
deffunc H1( Element of G) -> Element of the carrier 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 = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of G,G ;
take f ; ::_thesis: for x being Element of G holds f . x = a * x
thus for x being Element of G holds f . x = a * x by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = a * x ) & ( for x being Element of G holds b2 . x = a * x ) holds
b1 = b2
proof
let f, g be Function of G,G; ::_thesis: ( ( for x being Element of G holds f . x = a * x ) & ( for x being Element of G holds g . x = a * x ) implies f = g )
assume 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 ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of G implies f . x = g . x )
assume x in the carrier of G ; ::_thesis: f . x = g . x
then reconsider y = x as Element of G ;
thus f . x = a * y by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:12; ::_thesis: verum
end;
func * a -> Function of G,G means :Def2: :: TOPGRP_1:def 2
for x being Element of G holds it . x = x * a;
existence
ex b1 being Function of G,G st
for x being Element of G holds b1 . x = x * a
proof
deffunc H1( Element of G) -> Element of the carrier 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 = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of G,G ;
take f ; ::_thesis: for x being Element of G holds f . x = x * a
thus for x being Element of G holds f . x = x * a by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = x * a ) & ( for x being Element of G holds b2 . x = x * a ) holds
b1 = b2
proof
let f, g be Function of G,G; ::_thesis: ( ( for x being Element of G holds f . x = x * a ) & ( for x being Element of G holds g . x = x * a ) implies f = g )
assume 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 ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of G implies f . x = g . x )
assume x in the carrier of G ; ::_thesis: f . x = g . x
then reconsider y = x as Element of G ;
thus f . x = y * a by A5
.= g . x by A6 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines * TOPGRP_1:def_1_:_
for G being non empty multMagma
for a being Element of G
for b3 being Function of G,G holds
( b3 = a * iff for x being Element of G holds b3 . x = a * x );
:: deftheorem Def2 defines * TOPGRP_1:def_2_:_
for G being non empty multMagma
for a being Element of G
for b3 being Function of G,G holds
( b3 = * a iff for x being Element of G holds b3 . x = x * a );
registration
let G be Group;
let a be Element of G;
clustera * -> one-to-one onto ;
coherence
( a * is one-to-one & a * is onto )
proof
set f = a * ;
A1: dom (a *) = the carrier of G by FUNCT_2:def_1;
hereby :: according to FUNCT_1:def_4 ::_thesis: a * is onto
let x1, x2 be set ; ::_thesis: ( x1 in dom (a *) & x2 in dom (a *) & (a *) . x1 = (a *) . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom (a *) & x2 in dom (a *) ) and
A3: (a *) . x1 = (a *) . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of G by A2;
A4: ( (a *) . y1 = a * y1 & (a *) . 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 ; ::_thesis: verum
end;
thus rng (a *) c= the carrier of G ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (a *)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng (a *) )
assume y in the carrier of G ; ::_thesis: y in rng (a *)
then reconsider y1 = y as Element of G ;
(a *) . ((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 y in rng (a *) by A1, FUNCT_1:def_3; ::_thesis: verum
end;
cluster * a -> one-to-one onto ;
coherence
( * a is one-to-one & * a is onto )
proof
set f = * a;
A5: dom (* a) = the carrier of G by FUNCT_2:def_1;
hereby :: according to FUNCT_1:def_4 ::_thesis: * a is onto
let x1, x2 be set ; ::_thesis: ( x1 in dom (* a) & x2 in dom (* a) & (* a) . x1 = (* a) . x2 implies x1 = x2 )
assume that
A6: ( x1 in dom (* a) & x2 in dom (* a) ) and
A7: (* a) . x1 = (* a) . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of G by A6;
A8: ( (* a) . y1 = y1 * a & (* a) . 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 ; ::_thesis: verum
end;
thus rng (* a) c= the carrier of G ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (* a)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng (* a) )
assume y in the carrier of G ; ::_thesis: y in rng (* a)
then reconsider y1 = y as Element of G ;
(* a) . (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 y in rng (* a) by A5, FUNCT_1:def_3; ::_thesis: verum
end;
end;
theorem Th16: :: TOPGRP_1:16
for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (h *) .: P = h * P
proof
let H be non empty multMagma ; ::_thesis: for P being Subset of H
for h being Element of H holds (h *) .: P = h * P
let P be Subset of H; ::_thesis: for h being Element of H holds (h *) .: P = h * P
let h be Element of H; ::_thesis: (h *) .: P = h * P
set f = h * ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: h * P c= (h *) .: P
let y be set ; ::_thesis: ( y in (h *) .: P implies y in h * P )
assume y in (h *) .: P ; ::_thesis: y in h * P
then consider x being set such that
A1: x in dom (h *) and
A2: ( x in P & y = (h *) . x ) by FUNCT_1:def_6;
reconsider x = x as Element of H by A1;
(h *) . x = h * x by Def1;
hence y in h * P by A2, GROUP_2:27; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in h * P or y in (h *) .: P )
assume y in h * P ; ::_thesis: 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 (h *) = the carrier of H & (h *) . s = h * s ) by Def1, FUNCT_2:def_1;
hence y in (h *) .: P by A3, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th17: :: TOPGRP_1:17
for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (* h) .: P = P * h
proof
let H be non empty multMagma ; ::_thesis: for P being Subset of H
for h being Element of H holds (* h) .: P = P * h
let P be Subset of H; ::_thesis: for h being Element of H holds (* h) .: P = P * h
let h be Element of H; ::_thesis: (* h) .: P = P * h
set f = * h;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P * h c= (* h) .: P
let y be set ; ::_thesis: ( y in (* h) .: P implies y in P * h )
assume y in (* h) .: P ; ::_thesis: y in P * h
then consider x being set such that
A1: x in dom (* h) and
A2: ( x in P & y = (* h) . x ) by FUNCT_1:def_6;
reconsider x = x as Element of H by A1;
(* h) . x = x * h by Def2;
hence y in P * h by A2, GROUP_2:28; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P * h or y in (* h) .: P )
assume y in P * h ; ::_thesis: y in (* h) .: P
then consider s being Element of H such that
A3: ( y = s * h & s in P ) by GROUP_2:28;
( dom (* h) = the carrier of H & (* h) . s = s * h ) by Def2, FUNCT_2:def_1;
hence y in (* h) .: P by A3, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th18: :: TOPGRP_1:18
for G being Group
for a being Element of G holds (a *) /" = (a ") *
proof
let G be Group; ::_thesis: for a being Element of G holds (a *) /" = (a ") *
let a be Element of G; ::_thesis: (a *) /" = (a ") *
set f = a * ;
set g = (a ") * ;
A1: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_
((a_*)_/")_._y_=_((a_")_*)_._y
reconsider h = a * as Function ;
let y be set ; ::_thesis: ( y in the carrier of G implies ((a *) /") . y = ((a ") *) . y )
assume y in the carrier of G ; ::_thesis: ((a *) /") . y = ((a ") *) . y
then reconsider y1 = y as Element of G ;
rng (a *) = the carrier of G by FUNCT_2:def_3;
then A2: y1 in rng (a *) ;
dom (a *) = the carrier of G by FUNCT_2:def_1;
then A3: ( ((a ") *) . y1 in dom (a *) & ((a *) /") . y1 in dom (a *) ) ;
(a *) . (((a ") *) . y) = a * (((a ") *) . 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
.= (a *) . (((a *) /") . y) by TOPS_2:def_4 ;
hence ((a *) /") . y = ((a ") *) . y by A3, FUNCT_1:def_4; ::_thesis: verum
end;
( dom ((a *) /") = the carrier of G & dom ((a ") *) = the carrier of G ) by FUNCT_2:def_1;
hence (a *) /" = (a ") * by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th19: :: TOPGRP_1:19
for G being Group
for a being Element of G holds (* a) /" = * (a ")
proof
let G be Group; ::_thesis: for a being Element of G holds (* a) /" = * (a ")
let a be Element of G; ::_thesis: (* a) /" = * (a ")
set f = * a;
set g = * (a ");
A1: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_
((*_a)_/")_._y_=_(*_(a_"))_._y
reconsider h = * a as Function ;
let y be set ; ::_thesis: ( y in the carrier of G implies ((* a) /") . y = (* (a ")) . y )
assume y in the carrier of G ; ::_thesis: ((* a) /") . y = (* (a ")) . y
then reconsider y1 = y as Element of G ;
rng (* a) = the carrier of G by FUNCT_2:def_3;
then A2: y1 in rng (* a) ;
dom (* a) = the carrier of G by FUNCT_2:def_1;
then A3: ( (* (a ")) . y1 in dom (* a) & ((* a) /") . y1 in dom (* a) ) ;
(* a) . ((* (a ")) . y) = ((* (a ")) . 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
.= (* a) . (((* a) /") . y) by TOPS_2:def_4 ;
hence ((* a) /") . y = (* (a ")) . y by A3, FUNCT_1:def_4; ::_thesis: verum
end;
( dom ((* a) /") = the carrier of G & dom (* (a ")) = the carrier of G ) by FUNCT_2:def_1;
hence (* a) /" = * (a ") by A1, FUNCT_1:2; ::_thesis: verum
end;
begin
registration
let T be TopStruct ;
cluster(id T) /" -> continuous ;
coherence
(id T) /" is continuous by Th2;
end;
theorem Th20: :: TOPGRP_1:20
for T being TopStruct holds id T is being_homeomorphism
proof
let T be TopStruct ; ::_thesis: id T is being_homeomorphism
thus ( dom (id T) = [#] T & rng (id T) = [#] T ) by RELAT_1:45; :: according to TOPS_2:def_5 ::_thesis: ( id T is one-to-one & id T is continuous & (id T) /" is continuous )
thus ( id T is one-to-one & id T is continuous & (id T) /" is continuous ) ; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
let p be Point of T;
cluster -> non empty for a_neighborhood of p;
coherence
for b1 being a_neighborhood of p holds not b1 is empty
proof
let N be a_neighborhood of p; ::_thesis: not N is empty
p in Int N by CONNSP_2:def_1;
hence not N is empty ; ::_thesis: verum
end;
end;
theorem Th21: :: TOPGRP_1:21
for T being non empty TopSpace
for p being Point of T holds [#] T is a_neighborhood of p
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds [#] T is a_neighborhood of p
let p be Point of T; ::_thesis: [#] T is a_neighborhood of p
Int ([#] T) = the carrier of T by TOPS_1:15;
hence p in Int ([#] T) ; :: according to CONNSP_2:def_1 ::_thesis: verum
end;
registration
let T be non empty TopSpace;
let p be Point of T;
cluster non empty open for a_neighborhood of p;
existence
ex b1 being a_neighborhood of p st
( not b1 is empty & b1 is open )
proof
reconsider B = [#] T as a_neighborhood of p by Th21;
take B ; ::_thesis: ( not B is empty & B is open )
thus ( not B is empty & B is open ) ; ::_thesis: verum
end;
end;
theorem :: TOPGRP_1:22
for S, T being non empty TopSpace
for f being Function of S,T st f is open holds
for p being Point of S
for 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; ::_thesis: for f being Function of S,T st f is open holds
for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let f be Function of S,T; ::_thesis: ( f is open implies for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P )
assume A1: for A being Subset of S st A is open holds
f .: A is open ; :: according to T_0TOPSP:def_2 ::_thesis: for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let p be Point of S; ::_thesis: for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let P be a_neighborhood of p; ::_thesis: ex R being open a_neighborhood of f . p st R c= f .: 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 ; ::_thesis: R c= f .: P
thus R c= f .: P by RELAT_1:123, TOPS_1:16; ::_thesis: verum
end;
theorem :: TOPGRP_1:23
for S, T being non empty TopSpace
for f being Function of S,T st ( for p being Point of S
for 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; ::_thesis: for f being Function of S,T st ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) holds
f is open
let f be Function of S,T; ::_thesis: ( ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) implies f is open )
assume A1: for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ; ::_thesis: f is open
let A be Subset of S; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open )
assume A2: A is open ; ::_thesis: f .: 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 ; ::_thesis: ( x in f .: A iff ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) )
hereby ::_thesis: ( ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )
assume x in f .: A ; ::_thesis: ex K being Element of bool the carrier of T st
( K is open & K c= f .: A & x in K )
then consider a being set 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; ::_thesis: ( K is open & K c= f .: A & x in K )
Int R c= R by TOPS_1:16;
then A10: K c= f .: V by A9, XBOOLE_1:1;
thus K is open ; ::_thesis: ( K c= f .: A & x in K )
f .: V c= f .: A by A7, RELAT_1:123;
hence K c= f .: A by A10, XBOOLE_1:1; ::_thesis: x in K
thus x in K by A5, CONNSP_2:def_1; ::_thesis: verum
end;
thus ( ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; ::_thesis: verum
end;
hence f .: A is open by TOPS_1:25; ::_thesis: verum
end;
theorem :: TOPGRP_1:24
for S, T being non empty TopStruct
for 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 ; ::_thesis: for 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 ) ) ) )
let f be Function of S,T; ::_thesis: ( 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 ) ) ) )
hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) ) ) )
hence A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of T holds
( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) )
let P be Subset of T; ::_thesis: ( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) )
hereby ::_thesis: ( f " P is closed implies P is closed )
assume A3: P is closed ; ::_thesis: f " P is closed
f is continuous by A1, TOPS_2:def_5;
hence f " P is closed by A3, PRE_TOPC:def_6; ::_thesis: verum
end;
assume f " P is closed ; ::_thesis: P is closed
then f .: (f " P) is closed by A1, TOPS_2:58;
hence P is closed by A2, FUNCT_1:77; ::_thesis: verum
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 ) ; ::_thesis: f is being_homeomorphism
thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A4, A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f /" is continuous )
thus f is continuous ::_thesis: f /" is continuous
proof
let P be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or f " P is closed )
thus ( not P is closed or f " P is closed ) by A7; ::_thesis: verum
end;
let R be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not R is closed or (f /") " R is closed )
assume A8: R is closed ; ::_thesis: (f /") " 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, FUNCT_1:def_4;
then A9: f " (f .: R) = R by T_0TOPSP:1;
(f /") " R = f .: R by A5, A6, TOPS_2:54;
hence (f /") " R is closed by A7, A8, A9; ::_thesis: verum
end;
theorem Th25: :: TOPGRP_1:25
for S, T being non empty TopStruct
for 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 ; ::_thesis: for 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 ) ) ) )
let f be Function of S,T; ::_thesis: ( 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 ) ) ) )
A1: [#] T <> {} ;
A2: [#] S <> {} ;
hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism )
assume A3: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of S holds
( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) ) ) )
hence A4: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of S holds
( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) )
let P be Subset of S; ::_thesis: ( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) )
A5: ( f " (f .: P) c= P & P c= f " (f .: P) ) by A4, FUNCT_1:76, FUNCT_1:82;
A6: f /" is continuous by A3, TOPS_2:def_5;
hereby ::_thesis: ( f .: P is open implies P is open )
assume A7: P is open ; ::_thesis: f .: P is open
f is onto by A4, FUNCT_2:def_3;
then (f /") " P = (f ") " 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; ::_thesis: verum
end;
assume A8: f .: P is open ; ::_thesis: P is open
f is continuous by A3, TOPS_2:def_5;
then f " (f .: P) is open by A1, A8, TOPS_2:43;
hence P is open by A5, XBOOLE_0:def_10; ::_thesis: verum
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 ) ; ::_thesis: f is being_homeomorphism
now__::_thesis:_for_B_being_Subset_of_T_st_B_is_open_holds_
f_"_B_is_open
let B be Subset of T; ::_thesis: ( B is open implies f " B is open )
assume A13: B is open ; ::_thesis: f " B is open
B = f .: (f " B) by A10, FUNCT_1:77;
hence f " B is open by A12, A13; ::_thesis: verum
end;
then A14: f is continuous by A1, TOPS_2:43;
now__::_thesis:_for_B_being_Subset_of_S_st_B_is_open_holds_
(f_/")_"_B_is_open
let B be Subset of S; ::_thesis: ( B is open implies (f /") " B is open )
assume A15: B is open ; ::_thesis: (f /") " B is open
f is onto by A10, FUNCT_2:def_3;
then (f /") " B = (f ") " B by A11, TOPS_2:def_4
.= f .: B by A11, FUNCT_1:84 ;
hence (f /") " B is open by A12, A15; ::_thesis: verum
end;
then f /" is continuous by A2, TOPS_2:43;
hence f is being_homeomorphism by A9, A10, A11, A14, TOPS_2:def_5; ::_thesis: verum
end;
theorem :: TOPGRP_1:26
for S, T being non empty TopStruct
for 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 ; ::_thesis: for 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 ) ) ) )
let f be Function of S,T; ::_thesis: ( 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 ) ) ) )
A1: [#] T <> {} ;
hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism )
assume A2: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) ) ) )
hence A3: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of T holds
( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) )
let P be Subset of T; ::_thesis: ( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) )
hereby ::_thesis: ( f " P is open implies P is open )
assume A4: P is open ; ::_thesis: f " P is open
f is continuous by A2, TOPS_2:def_5;
hence f " P is open by A1, A4, TOPS_2:43; ::_thesis: verum
end;
assume f " P is open ; ::_thesis: P is open
then f .: (f " P) is open by A2, Th25;
hence P is open by A3, FUNCT_1:77; ::_thesis: verum
end;
assume that
A5: dom f = [#] S and
A6: rng f = [#] T and
A7: f is one-to-one and
A8: for P being Subset of T holds
( P is open iff f " P is open ) ; ::_thesis: f is being_homeomorphism
A9: now__::_thesis:_for_R_being_Subset_of_S_st_R_is_open_holds_
(f_/")_"_R_is_open
let R be Subset of S; ::_thesis: ( R is open implies (f /") " R is open )
assume A10: R is open ; ::_thesis: (f /") " R is open
for x1, x2 being Element of S st x1 in R & f . x1 = f . x2 holds
x2 in R by A5, A7, FUNCT_1:def_4;
then A11: f " (f .: R) = R by T_0TOPSP:1;
(f /") " R = f .: R by A6, A7, TOPS_2:54;
hence (f /") " R is open by A8, A10, A11; ::_thesis: verum
end;
thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A5, A6, A7; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f /" is continuous )
thus f is continuous by A1, A8, TOPS_2:43; ::_thesis: f /" is continuous
[#] S <> {} ;
hence f /" is continuous by A9, TOPS_2:43; ::_thesis: verum
end;
theorem :: TOPGRP_1:27
for S being TopSpace
for T being non empty TopSpace
for 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; ::_thesis: for T being non empty TopSpace
for 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) )
let T be non empty TopSpace; ::_thesis: for 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) )
let f be Function of S,T; ::_thesis: ( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) )
A1: [#] T <> {} ;
hereby ::_thesis: ( ( for P being Subset of T holds f " (Int P) c= Int (f " P) ) implies f is continuous )
assume A2: f is continuous ; ::_thesis: for P being Subset of T holds f " (Int P) c= Int (f " P)
let P be Subset of T; ::_thesis: f " (Int P) c= Int (f " P)
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; ::_thesis: verum
end;
assume A4: for P being Subset of T holds f " (Int P) c= Int (f " P) ; ::_thesis: f is continuous
now__::_thesis:_for_P_being_Subset_of_T_st_P_is_open_holds_
f_"_P_is_open
let P be Subset of T; ::_thesis: ( P is open implies f " P is open )
assume P is open ; ::_thesis: f " 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; ::_thesis: verum
end;
hence f is continuous by A1, TOPS_2:43; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster non empty dense for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is dense )
proof
take [#] T ; ::_thesis: ( not [#] T is empty & [#] T is dense )
thus ( not [#] T is empty & [#] T is dense ) ; ::_thesis: verum
end;
end;
theorem Th28: :: TOPGRP_1:28
for S, T being non empty TopSpace
for f being Function of S,T
for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T
for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
let f be Function of S,T; ::_thesis: for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
let A be dense Subset of S; ::_thesis: ( f is being_homeomorphism implies f .: A is dense )
assume A1: f is being_homeomorphism ; ::_thesis: f .: A is dense
A2: rng f = [#] T by A1, TOPS_2:def_5;
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 ;
:: according to TOPS_1:def_3 ::_thesis: verum
end;
theorem Th29: :: TOPGRP_1:29
for S, T being non empty TopSpace
for f being Function of S,T
for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T
for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
let f be Function of S,T; ::_thesis: for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
let A be dense Subset of T; ::_thesis: ( f is being_homeomorphism implies f " A is dense )
assume A1: f is being_homeomorphism ; ::_thesis: f " A is dense
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 ; :: according to TOPS_1:def_3 ::_thesis: verum
end;
registration
let S, T be TopStruct ;
cluster Function-like quasi_total being_homeomorphism -> one-to-one onto continuous for Element of bool [: the carrier of S, the carrier of T:];
coherence
for b1 being Function of S,T st b1 is being_homeomorphism holds
( b1 is onto & b1 is one-to-one & b1 is continuous )
proof
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies ( f is onto & f is one-to-one & f is continuous ) )
assume A1: f is being_homeomorphism ; ::_thesis: ( f is onto & f is one-to-one & f is continuous )
then rng f = [#] T by TOPS_2:def_5;
hence rng f = the carrier of T ; :: according to FUNCT_2:def_3 ::_thesis: ( f is one-to-one & f is continuous )
thus ( f is one-to-one & f is continuous ) by A1, TOPS_2:def_5; ::_thesis: verum
end;
end;
registration
let S, T be non empty TopStruct ;
cluster Function-like quasi_total being_homeomorphism -> open for Element of bool [: the carrier of S, the carrier of T:];
coherence
for b1 being Function of S,T st b1 is being_homeomorphism holds
b1 is open
proof
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f is open )
assume A1: f is being_homeomorphism ; ::_thesis: f is open
let A be Subset of S; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open )
thus ( not A is open or f .: A is open ) by A1, Th25; ::_thesis: verum
end;
end;
registration
let T be TopStruct ;
cluster Relation-like the carrier of T -defined the carrier of T -valued Function-like V14( the carrier of T) quasi_total being_homeomorphism for Element of bool [: the carrier of T, the carrier of T:];
existence
ex b1 being Function of T,T st b1 is being_homeomorphism
proof
take id T ; ::_thesis: id T is being_homeomorphism
thus id T is being_homeomorphism by Th20; ::_thesis: verum
end;
end;
registration
let T be TopStruct ;
let f be being_homeomorphism Function of T,T;
clusterf /" -> being_homeomorphism ;
coherence
f /" is being_homeomorphism
proof
percases ( not T is empty or T is empty ) ;
suppose not T is empty ; ::_thesis: f /" is being_homeomorphism
hence f /" is being_homeomorphism by TOPS_2:56; ::_thesis: verum
end;
suppose T is empty ; ::_thesis: f /" is being_homeomorphism
then A1: the carrier of T is empty ;
f /" = f " by TOPS_2:def_4
.= id T by A1, RELAT_1:55 ;
hence f /" is being_homeomorphism by Th20; ::_thesis: verum
end;
end;
end;
end;
begin
definition
let S, T be TopStruct ;
assume A1: S,T are_homeomorphic ;
mode Homeomorphism of S,T -> Function of S,T means :Def3: :: TOPGRP_1:def 3
it is being_homeomorphism ;
existence
ex b1 being Function of S,T st b1 is being_homeomorphism by A1, T_0TOPSP:def_1;
end;
:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def_3_:_
for S, T being TopStruct st S,T are_homeomorphic holds
for b3 being Function of S,T holds
( b3 is Homeomorphism of S,T iff b3 is being_homeomorphism );
definition
let T be TopStruct ;
mode Homeomorphism of T -> Function of T,T means :Def4: :: TOPGRP_1:def 4
it is being_homeomorphism ;
existence
ex b1 being Function of T,T st b1 is being_homeomorphism
proof
A1: id T is being_homeomorphism by Th20;
then T,T are_homeomorphic by T_0TOPSP:def_1;
then reconsider f = id T as Homeomorphism of T,T by A1, Def3;
f is being_homeomorphism by Th20;
hence ex b1 being Function of T,T st b1 is being_homeomorphism ; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def_4_:_
for T being TopStruct
for b2 being Function of T,T holds
( b2 is Homeomorphism of T iff b2 is being_homeomorphism );
definition
let T be TopStruct ;
:: original: Homeomorphism
redefine mode Homeomorphism of T -> Homeomorphism of T,T;
coherence
for b1 being Homeomorphism of T holds b1 is Homeomorphism of T,T
proof
let f be Homeomorphism of T; ::_thesis: f is Homeomorphism of T,T
A1: f is being_homeomorphism by Def4;
then T,T are_homeomorphic by T_0TOPSP:def_1;
hence f is Homeomorphism of T,T by A1, Def3; ::_thesis: verum
end;
end;
definition
let T be TopStruct ;
:: original: id
redefine func id T -> Homeomorphism of T,T;
coherence
id T is Homeomorphism of T,T
proof
id T is being_homeomorphism by Th20;
hence T,T are_homeomorphic by T_0TOPSP:def_1; :: according to TOPGRP_1:def_3 ::_thesis: id T is being_homeomorphism
thus id T is being_homeomorphism by Th20; ::_thesis: verum
end;
end;
definition
let T be TopStruct ;
:: original: id
redefine func id T -> Homeomorphism of T;
coherence
id T is Homeomorphism of T
proof
thus id T is being_homeomorphism by Th20; :: according to TOPGRP_1:def_4 ::_thesis: verum
end;
end;
registration
let T be TopStruct ;
cluster -> being_homeomorphism for Homeomorphism of T;
coherence
for b1 being Homeomorphism of T holds b1 is being_homeomorphism by Def4;
end;
theorem Th30: :: TOPGRP_1:30
for T being TopStruct
for f being Homeomorphism of T holds f /" is Homeomorphism of T
proof
let T be TopStruct ; ::_thesis: for f being Homeomorphism of T holds f /" is Homeomorphism of T
let f be Homeomorphism of T; ::_thesis: f /" is Homeomorphism of T
thus f /" is being_homeomorphism ; :: according to TOPGRP_1:def_4 ::_thesis: verum
end;
Lm2: for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism
proof
let T be TopStruct ; ::_thesis: for f being Function of T,T st T is empty holds
f is being_homeomorphism
let f be Function of T,T; ::_thesis: ( T is empty implies f is being_homeomorphism )
assume A1: T is empty ; ::_thesis: f is being_homeomorphism
then f = {}
.= id T by A1 ;
hence f is being_homeomorphism ; ::_thesis: verum
end;
theorem Th31: :: TOPGRP_1:31
for T being TopStruct
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
proof
let T be TopStruct ; ::_thesis: for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
let f, g be Homeomorphism of T; ::_thesis: f * g is Homeomorphism of T
( not T is empty or T is empty ) ;
hence f * g is being_homeomorphism by TOPS_2:57; :: according to TOPGRP_1:def_4 ::_thesis: verum
end;
definition
let T be TopStruct ;
func HomeoGroup T -> strict multMagma means :Def5: :: TOPGRP_1:def 5
for x being set holds
( ( x in the carrier of it implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of it ) & ( for f, g being Homeomorphism of T holds the multF of it . (f,g) = g * f ) );
existence
ex b1 being strict multMagma st
for x being set holds
( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) )
proof
defpred S1[ set ] means $1 is Homeomorphism of T;
consider A being set such that
A1: for q being set holds
( q in A iff ( q in Funcs ( the carrier of T, the carrier of T) & S1[q] ) ) from XBOOLE_0:sch_1();
A2: now__::_thesis:_for_f_being_Homeomorphism_of_T_holds_f_in_A
let f be Homeomorphism of T; ::_thesis: f in A
f in Funcs ( the carrier of T, the carrier of T) by FUNCT_2:9;
hence f in A by A1; ::_thesis: verum
end;
then reconsider A = A as non empty set ;
defpred S2[ 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 S2[x,y,z]
proof
let x, y be Element of A; ::_thesis: ex z being Element of A st S2[x,y,z]
reconsider x1 = x, y1 = y as Homeomorphism of T by A1;
y1 * x1 is Homeomorphism of T by Th31;
then reconsider z = y1 * x1 as Element of A by A2;
take z ; ::_thesis: S2[x,y,z]
take x1 ; ::_thesis: ex g being Homeomorphism of T st
( x = x1 & y = g & z = g * x1 )
take y1 ; ::_thesis: ( x = x1 & y = y1 & z = y1 * x1 )
thus ( x = x1 & y = y1 & z = y1 * x1 ) ; ::_thesis: verum
end;
consider o being BinOp of A such that
A4: for a, b being Element of A holds S2[a,b,o . (a,b)] from BINOP_1:sch_3(A3);
take G = multMagma(# A,o #); ::_thesis: for x being set holds
( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) )
let x be set ; ::_thesis: ( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) )
thus ( x in the carrier of G iff x is Homeomorphism of T ) by A1, A2; ::_thesis: for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f
let f, g be Homeomorphism of T; ::_thesis: the multF of G . (f,g) = g * f
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 the multF of G . (f,g) = g * f ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict multMagma st ( for x being set holds
( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) ) ) & ( for x being set holds
( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is Homeomorphism of T;
let A, B be strict multMagma ; ::_thesis: ( ( for x being set holds
( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . (f,g) = g * f ) ) ) & ( for x being set holds
( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . (f,g) = g * f ) ) ) implies A = B )
assume that
A5: for x being set holds
( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . (f,g) = g * f ) ) and
A6: for x being set holds
( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . (f,g) = g * f ) ) ; ::_thesis: A = B
A7: for x being set holds
( x in the carrier of B iff S1[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 ; ::_thesis: ( c in the carrier of A & d in the carrier of A implies the multF of A . (c,d) = the multF of B . (c,d) )
assume ( c in the carrier of A & d in the carrier of A ) ; ::_thesis: the multF of A . (c,d) = the multF of B . (c,d)
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 ; ::_thesis: verum
end;
A9: for x being set holds
( x in the carrier of A iff S1[x] ) by A5;
the carrier of A = the carrier of B from XBOOLE_0:sch_2(A9, A7);
hence A = B by A8, BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def_5_:_
for T being TopStruct
for b2 being strict multMagma holds
( b2 = HomeoGroup T iff for x being set holds
( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) );
registration
let T be TopStruct ;
cluster HomeoGroup T -> non empty strict ;
coherence
not HomeoGroup T is empty
proof
id T is Homeomorphism of T ;
hence not the carrier of (HomeoGroup T) is empty by Def5; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem :: TOPGRP_1:32
for T being TopStruct
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 -> strict Group-like associative ;
coherence
( HomeoGroup T is Group-like & HomeoGroup T is associative )
proof
set G = HomeoGroup T;
set o = the multF of (HomeoGroup T);
thus HomeoGroup T is Group-like ::_thesis: HomeoGroup T is associative
proof
reconsider e = id T as Element of (HomeoGroup T) by Def5;
take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (HomeoGroup T) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (HomeoGroup T) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (HomeoGroup T); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (HomeoGroup T) st
( h * b1 = e & b1 * h = e ) )
reconsider h1 = h, e1 = e as Homeomorphism of T by Def5;
thus h * e = e1 * h1 by Def5
.= h by FUNCT_2:17 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (HomeoGroup T) st
( h * b1 = e & b1 * h = e ) )
thus e * h = h1 * e1 by Def5
.= h by FUNCT_2:17 ; ::_thesis: ex b1 being Element of the carrier of (HomeoGroup T) st
( h * b1 = e & b1 * h = e )
reconsider h1 = h as Homeomorphism of T by Def5;
A1: dom h1 = [#] T by TOPS_2:def_5;
h1 /" is Homeomorphism of T by Th30;
then reconsider g = h1 /" as Element of (HomeoGroup T) by Def5;
reconsider g1 = g as Homeomorphism of T by Def5;
take g ; ::_thesis: ( h * g = e & g * h = e )
A2: rng h1 = [#] T by TOPS_2:def_5;
thus h * g = g1 * h1 by Def5
.= e by A1, A2, TOPS_2:52 ; ::_thesis: g * h = e
thus g * h = h1 * g1 by Def5
.= e by A2, TOPS_2:52 ; ::_thesis: verum
end;
let x, y, z be Element of (HomeoGroup T); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider f = x, g = y as Homeomorphism of T by Def5;
reconsider p = g * f, r = z as Homeomorphism of T by Def5, Th31;
reconsider a = r * g as Homeomorphism of T by Th31;
thus (x * y) * z = the multF of (HomeoGroup T) . ((g * f),z) by Def5
.= r * p by Def5
.= (r * g) * f by RELAT_1:36
.= the multF of (HomeoGroup T) . (f,a) by Def5
.= x * (y * z) by Def5 ; ::_thesis: verum
end;
end;
theorem Th33: :: TOPGRP_1:33
for T being TopStruct holds id T = 1_ (HomeoGroup T)
proof
let T be TopStruct ; ::_thesis: id T = 1_ (HomeoGroup T)
set G = HomeoGroup T;
reconsider e = id T as Element of (HomeoGroup T) by Def5;
now__::_thesis:_for_h_being_Element_of_(HomeoGroup_T)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of (HomeoGroup T); ::_thesis: ( h * e = h & e * h = h )
reconsider h1 = h as Homeomorphism of T by Def5;
thus h * e = (id T) * h1 by Def5
.= h by FUNCT_2:17 ; ::_thesis: e * h = h
thus e * h = h1 * (id T) by Def5
.= h by FUNCT_2:17 ; ::_thesis: verum
end;
hence id T = 1_ (HomeoGroup T) by GROUP_1:4; ::_thesis: verum
end;
theorem :: TOPGRP_1:34
for T being TopStruct
for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
proof
let T be TopStruct ; ::_thesis: for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
let f be Homeomorphism of T; ::_thesis: for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
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 (HomeoGroup T) by Def5;
A3: rng f = [#] T by TOPS_2:def_5;
let a be Element of (HomeoGroup T); ::_thesis: ( f = a implies a " = f /" )
assume A4: f = a ; ::_thesis: a " = f /"
A5: g * a = f * (f /") by A4, A2, Def5
.= id T by A3, TOPS_2:52
.= 1_ (HomeoGroup T) by Th33 ;
a * g = (f /") * f by A4, A2, Def5
.= id T by A1, A3, TOPS_2:52
.= 1_ (HomeoGroup T) by Th33 ;
hence a " = f /" by A5, GROUP_1:5; ::_thesis: verum
end;
definition
let T be TopStruct ;
attrT is homogeneous means :Def6: :: TOPGRP_1:def 6
for p, q being Point of T ex f being Homeomorphism of T st f . p = q;
end;
:: deftheorem Def6 defines homogeneous TOPGRP_1:def_6_:_
for T being TopStruct holds
( T is homogeneous iff for p, q being Point of T ex f being Homeomorphism of T st f . p = q );
registration
cluster1 -element -> 1 -element homogeneous for TopStruct ;
coherence
for b1 being 1 -element TopStruct holds b1 is homogeneous
proof
let T be 1 -element TopStruct ; ::_thesis: T is homogeneous
let p, q be Point of T; :: according to TOPGRP_1:def_6 ::_thesis: ex f being Homeomorphism of T st f . p = q
take id T ; ::_thesis: (id T) . p = q
thus (id T) . p = q by STRUCT_0:def_10; ::_thesis: verum
end;
end;
theorem :: TOPGRP_1:35
for T being non empty homogeneous TopSpace st ex p being Point of T st {p} is closed holds
T is T_1
proof
let T be non empty homogeneous TopSpace; ::_thesis: ( ex p being Point of T st {p} is closed implies T is T_1 )
given p being Point of T such that A1: {p} is closed ; ::_thesis: T is T_1
now__::_thesis:_for_q_being_Point_of_T_holds_{q}_is_closed
let q be Point of T; ::_thesis: {q} is closed
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; ::_thesis: verum
end;
hence T is T_1 by URYSOHN1:19; ::_thesis: verum
end;
theorem Th36: :: TOPGRP_1:36
for T being non empty homogeneous 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 non empty homogeneous TopSpace; ::_thesis: ( 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 ) implies T is regular )
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 ) ; ::_thesis: T is regular
A2: [#] T <> {} ;
now__::_thesis:_for_A_being_open_Subset_of_T
for_q_being_Point_of_T_st_q_in_A_holds_
ex_fB_being_open_Subset_of_T_st_
(_q_in_fB_&_Cl_fB_c=_A_)
let A be open Subset of T; ::_thesis: for q being Point of T st q in A holds
ex fB being open Subset of T st
( q in fB & Cl fB c= A )
let q be Point of T; ::_thesis: ( q in A implies ex fB being open Subset of T st
( q in fB & Cl fB c= A ) )
assume A3: q in A ; ::_thesis: ex fB being open Subset of T st
( q in fB & Cl fB c= 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, Th25;
take fB = fB; ::_thesis: ( q in fB & Cl fB c= A )
thus q in fB by A4, A6, A9, FUNCT_1:def_6; ::_thesis: Cl fB c= A
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; ::_thesis: verum
end;
hence T is regular by URYSOHN1:21; ::_thesis: verum
end;
begin
definition
attrc1 is strict ;
struct TopGrStr -> multMagma , TopStruct ;
aggrTopGrStr(# carrier, multF, topology #) -> TopGrStr ;
end;
registration
let A be non empty set ;
let R be BinOp of A;
let T be Subset-Family of A;
cluster TopGrStr(# A,R,T #) -> non empty ;
coherence
not TopGrStr(# A,R,T #) is empty ;
end;
registration
let x be set ;
let R be BinOp of {x};
let T be Subset-Family of {x};
cluster TopGrStr(# {x},R,T #) -> trivial ;
coherence
TopGrStr(# {x},R,T #) is trivial ;
end;
registration
cluster1 -element -> 1 -element Group-like associative commutative for multMagma ;
coherence
for b1 being 1 -element multMagma holds
( b1 is Group-like & b1 is associative & b1 is commutative )
proof
let H be 1 -element multMagma ; ::_thesis: ( H is Group-like & H is associative & H is commutative )
hereby :: according to GROUP_1:def_2 ::_thesis: ( H is associative & H is commutative )
set e = the Element of H;
take e = the Element of H; ::_thesis: for h being Element of H holds
( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
let h be Element of H; ::_thesis: ( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h ) by STRUCT_0:def_10; ::_thesis: ex g being Element of H st
( h * g = e & g * h = e )
take g = e; ::_thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by STRUCT_0:def_10; ::_thesis: verum
end;
thus for x, y, z being Element of H holds (x * y) * z = x * (y * z) by STRUCT_0:def_10; :: according to GROUP_1:def_3 ::_thesis: H is commutative
let x, y be Element of H; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
thus x * y = y * x by STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
let a be set ;
cluster 1TopSp {a} -> trivial ;
coherence
1TopSp {a} is trivial ;
end;
registration
cluster non empty strict for TopGrStr ;
existence
ex b1 being TopGrStr st
( b1 is strict & not b1 is empty )
proof
set R = the BinOp of {{}};
set T = the Subset-Family of {{}};
take TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) ; ::_thesis: ( TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty )
thus ( TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty ) ; ::_thesis: verum
end;
end;
registration
cluster1 -element TopSpace-like strict for TopGrStr ;
existence
ex b1 being TopGrStr st
( b1 is strict & b1 is TopSpace-like & b1 is 1 -element )
proof
set R = the BinOp of {{}};
take TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) ; ::_thesis: ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element )
the carrier of (1TopSp {{}}) is 1 -element ;
hence ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element ) by TEX_2:7; ::_thesis: verum
end;
end;
definition
let G be non empty Group-like associative TopGrStr ;
attrG is UnContinuous means :Def7: :: TOPGRP_1:def 7
inverse_op G is continuous ;
end;
:: deftheorem Def7 defines UnContinuous TOPGRP_1:def_7_:_
for G being non empty Group-like associative TopGrStr holds
( G is UnContinuous iff inverse_op G is continuous );
definition
let G be TopSpace-like TopGrStr ;
attrG is BinContinuous means :Def8: :: TOPGRP_1:def 8
for f being Function of [:G,G:],G st f = the multF of G holds
f is continuous ;
end;
:: deftheorem Def8 defines BinContinuous TOPGRP_1:def_8_:_
for G being TopSpace-like TopGrStr holds
( G is BinContinuous iff for f being Function of [:G,G:],G st f = the multF of G holds
f is continuous );
registration
cluster non empty trivial V43() 1 -element TopSpace-like compact unital Group-like associative commutative homogeneous strict UnContinuous BinContinuous for TopGrStr ;
existence
ex b1 being 1 -element TopSpace-like Group-like associative TopGrStr st
( b1 is strict & b1 is commutative & b1 is UnContinuous & b1 is BinContinuous )
proof
set R = the BinOp of {{}};
1TopSp {{}} is 1 -element ;
then reconsider T = TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) as 1 -element TopSpace-like strict TopGrStr by TEX_2:7;
take T ; ::_thesis: ( T is strict & T is commutative & T is UnContinuous & T is BinContinuous )
thus ( T is strict & T is commutative ) ; ::_thesis: ( T is UnContinuous & T is BinContinuous )
hereby :: according to TOPGRP_1:def_7 ::_thesis: T is BinContinuous
set f = inverse_op T;
thus inverse_op T is continuous ::_thesis: verum
proof
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or (inverse_op T) " P1 is closed )
assume P1 is closed ; ::_thesis: (inverse_op T) " P1 is closed
percases ( (inverse_op T) " P1 = {} or (inverse_op T) " P1 = {{}} ) by ZFMISC_1:33;
suppose (inverse_op T) " P1 = {} ; ::_thesis: (inverse_op T) " P1 is closed
hence (inverse_op T) " P1 is closed ; ::_thesis: verum
end;
suppose (inverse_op T) " P1 = {{}} ; ::_thesis: (inverse_op T) " P1 is closed
then (inverse_op T) " P1 = [#] T ;
hence (inverse_op T) " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;
let f be Function of [:T,T:],T; :: according to TOPGRP_1:def_8 ::_thesis: ( f = the multF of T implies f is continuous )
assume f = the multF of T ; ::_thesis: f is continuous
A1: the carrier of [:T,T:] = [:{{}},{{}}:] by BORSUK_1:def_2
.= {[{},{}]} by ZFMISC_1:29 ;
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed )
assume P1 is closed ; ::_thesis: f " P1 is closed
percases ( f " P1 = {} or f " P1 = {[{},{}]} ) by A1, ZFMISC_1:33;
suppose f " P1 = {} ; ::_thesis: f " P1 is closed
hence f " P1 is closed ; ::_thesis: verum
end;
suppose f " P1 = {[{},{}]} ; ::_thesis: f " P1 is closed
then f " P1 = [#] [:T,T:] by A1;
hence f " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;
definition
mode TopGroup is non empty TopSpace-like Group-like associative TopGrStr ;
end;
definition
mode TopologicalGroup is UnContinuous BinContinuous TopGroup;
end;
theorem Th37: :: TOPGRP_1:37
for T being non empty TopSpace-like BinContinuous TopGrStr
for a, b being Element of T
for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
proof
let T be non empty TopSpace-like BinContinuous TopGrStr ; ::_thesis: for a, b being Element of T
for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
let W be a_neighborhood of a * b; ::_thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
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 holds
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 = B as open a_neighborhood of b by A8, CONNSP_2:def_1;
reconsider A = A as open a_neighborhood of a by A7, A9, CONNSP_2:def_1;
take A ; ::_thesis: ex B being open a_neighborhood of b st A * B c= W
take B ; ::_thesis: A * B c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in W )
assume x in A * B ; ::_thesis: x in W
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 x in W by A1; ::_thesis: verum
end;
theorem Th38: :: TOPGRP_1:38
for T being non empty TopSpace-like TopGrStr st ( for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) holds
T is BinContinuous
proof
let T be non empty TopSpace-like TopGrStr ; ::_thesis: ( ( for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) implies T is BinContinuous )
assume A1: for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ; ::_thesis: T is BinContinuous
let f be Function of [:T,T:],T; :: according to TOPGRP_1:def_8 ::_thesis: ( f = the multF of T implies f is continuous )
assume A2: f = the multF of T ; ::_thesis: f is continuous
for W being Point of [:T,T:]
for 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:]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
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 ; ::_thesis: f .: H c= G
thus f .: H c= G by A2, A4, Th15; ::_thesis: verum
end;
hence f is continuous by BORSUK_1:def_1; ::_thesis: verum
end;
theorem Th39: :: TOPGRP_1:39
for T being UnContinuous TopGroup
for a being Element of T
for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
proof
let T be UnContinuous TopGroup; ::_thesis: for a being Element of T
for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
let a be Element of T; ::_thesis: for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
let W be a_neighborhood of a " ; ::_thesis: ex A being open a_neighborhood of a st A " c= W
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 ; ::_thesis: A " c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in W )
assume x in A " ; ::_thesis: x in W
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 x in W by A1, A2; ::_thesis: verum
end;
theorem Th40: :: TOPGRP_1:40
for T being TopGroup st ( for a being Element of T
for 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; ::_thesis: ( ( for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ) implies T is UnContinuous )
assume A1: for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ; ::_thesis: T is UnContinuous
set f = inverse_op T;
for W being Point of T
for G being a_neighborhood of (inverse_op T) . W ex H being a_neighborhood of W st (inverse_op T) .: H c= G
proof
let a be Point of T; ::_thesis: for G being a_neighborhood of (inverse_op T) . a ex H being a_neighborhood of a st (inverse_op T) .: H c= G
let G be a_neighborhood of (inverse_op T) . a; ::_thesis: ex H being a_neighborhood of a st (inverse_op T) .: H c= G
(inverse_op T) . 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 ; ::_thesis: (inverse_op T) .: A c= G
thus (inverse_op T) .: A c= G by A2, Th10; ::_thesis: verum
end;
hence inverse_op T is continuous by BORSUK_1:def_1; :: according to TOPGRP_1:def_7 ::_thesis: verum
end;
theorem Th41: :: TOPGRP_1:41
for T being TopologicalGroup
for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
proof
let T be TopologicalGroup; ::_thesis: for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
let W be a_neighborhood of a * (b "); ::_thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
consider A being open a_neighborhood of a, B being open a_neighborhood of b " such that
A1: A * B c= W by Th37;
consider C being open a_neighborhood of b such that
A2: C " c= B by Th39;
take A ; ::_thesis: ex B being open a_neighborhood of b st A * (B ") c= W
take C ; ::_thesis: A * (C ") c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (C ") or x in W )
assume x in A * (C ") ; ::_thesis: x in W
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 x in W by A1, A3, A6; ::_thesis: verum
end;
theorem :: TOPGRP_1:42
for T being TopGroup st ( for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) holds
T is TopologicalGroup
proof
let T be TopGroup; ::_thesis: ( ( for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) implies T is TopologicalGroup )
assume A1: for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ; ::_thesis: T is TopologicalGroup
A2: for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W
proof
let a be Element of T; ::_thesis: for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W
let W be a_neighborhood of a " ; ::_thesis: ex A being a_neighborhood of a st A " c= W
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 ; ::_thesis: B " c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B " or x in W )
assume A4: x in B " ; ::_thesis: x in W
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 x in W by A3, A5; ::_thesis: verum
end;
for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
proof
let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
let W be a_neighborhood of a * b; ::_thesis: ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
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 ; ::_thesis: ex B being a_neighborhood of b st A * B c= W
take B1 ; ::_thesis: A * B1 c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B1 or x in W )
assume x in A * B1 ; ::_thesis: x in W
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 x in W by A6; ::_thesis: verum
end;
hence T is TopologicalGroup by A2, Th38, Th40; ::_thesis: verum
end;
registration
let G be non empty TopSpace-like BinContinuous TopGrStr ;
let a be Element of G;
clustera * -> continuous ;
coherence
a * is continuous
proof
set f = a * ;
for w being Point of G
for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A
proof
let w be Point of G; ::_thesis: for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A
let A be a_neighborhood of (a *) . w; ::_thesis: ex W being a_neighborhood of w st (a *) .: W c= A
(a *) . 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 Th37;
take W ; ::_thesis: (a *) .: W c= A
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in (a *) .: W or k in A )
assume k in (a *) .: W ; ::_thesis: k in A
then k in a * W by Th16;
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 k in A by A1; ::_thesis: verum
end;
hence a * is continuous by BORSUK_1:def_1; ::_thesis: verum
end;
cluster * a -> continuous ;
coherence
* a is continuous
proof
set f = * a;
for w being Point of G
for A being a_neighborhood of (* a) . w ex W being a_neighborhood of w st (* a) .: W c= A
proof
let w be Point of G; ::_thesis: for A being a_neighborhood of (* a) . w ex W being a_neighborhood of w st (* a) .: W c= A
let A be a_neighborhood of (* a) . w; ::_thesis: ex W being a_neighborhood of w st (* a) .: W c= A
(* a) . 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 Th37;
take W ; ::_thesis: (* a) .: W c= A
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in (* a) .: W or k in A )
assume k in (* a) .: W ; ::_thesis: k in A
then k in W * a by Th17;
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 k in A by A3; ::_thesis: verum
end;
hence * a is continuous by BORSUK_1:def_1; ::_thesis: verum
end;
end;
theorem Th43: :: TOPGRP_1:43
for G being BinContinuous TopGroup
for a being Element of G holds a * is Homeomorphism of G
proof
let G be BinContinuous TopGroup; ::_thesis: for a being Element of G holds a * is Homeomorphism of G
let a be Element of G; ::_thesis: a * is Homeomorphism of G
set f = a * ;
thus ( dom (a *) = [#] G & rng (a *) = [#] G & a * is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( a * is continuous & (a *) /" is continuous )
thus a * is continuous ; ::_thesis: (a *) /" is continuous
(a *) /" = (a ") * by Th18;
hence (a *) /" is continuous ; ::_thesis: verum
end;
theorem Th44: :: TOPGRP_1:44
for G being BinContinuous TopGroup
for a being Element of G holds * a is Homeomorphism of G
proof
let G be BinContinuous TopGroup; ::_thesis: for a being Element of G holds * a is Homeomorphism of G
let a be Element of G; ::_thesis: * a is Homeomorphism of G
set f = * a;
thus ( dom (* a) = [#] G & rng (* a) = [#] G & * a is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( * a is continuous & (* a) /" is continuous )
thus * a is continuous ; ::_thesis: (* a) /" is continuous
(* a) /" = * (a ") by Th19;
hence (* a) /" is continuous ; ::_thesis: verum
end;
definition
let G be BinContinuous TopGroup;
let a be Element of G;
:: original: *
redefine funca * -> Homeomorphism of G;
coherence
a * is Homeomorphism of G by Th43;
:: original: *
redefine func * a -> Homeomorphism of G;
coherence
* a is Homeomorphism of G by Th44;
end;
theorem Th45: :: TOPGRP_1:45
for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G
proof
let G be UnContinuous TopGroup; ::_thesis: inverse_op G is Homeomorphism of G
set f = inverse_op G;
thus ( dom (inverse_op G) = [#] G & rng (inverse_op G) = [#] G & inverse_op G is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( inverse_op G is continuous & (inverse_op G) /" is continuous )
thus inverse_op G is continuous by Def7; ::_thesis: (inverse_op G) /" is continuous
inverse_op G = (inverse_op G) " by Th14
.= (inverse_op G) /" by TOPS_2:def_4 ;
hence (inverse_op G) /" is continuous by Def7; ::_thesis: verum
end;
definition
let G be UnContinuous TopGroup;
:: original: inverse_op
redefine func inverse_op G -> Homeomorphism of G;
coherence
inverse_op G is Homeomorphism of G by Th45;
end;
registration
cluster non empty TopSpace-like Group-like associative BinContinuous -> homogeneous for TopGrStr ;
coherence
for b1 being TopGroup st b1 is BinContinuous holds
b1 is homogeneous
proof
let T be TopGroup; ::_thesis: ( T is BinContinuous implies T is homogeneous )
assume T is BinContinuous ; ::_thesis: T is homogeneous
then reconsider G = T as BinContinuous TopGroup ;
G is homogeneous
proof
let p, q be Point of G; :: according to TOPGRP_1:def_6 ::_thesis: ex f being Homeomorphism of G st f . p = q
take * ((p ") * q) ; ::_thesis: (* ((p ") * q)) . 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 ; ::_thesis: verum
end;
hence T is homogeneous ; ::_thesis: verum
end;
end;
theorem Th46: :: TOPGRP_1:46
for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds F * a is closed
proof
let G be BinContinuous TopGroup; ::_thesis: for F being closed Subset of G
for a being Element of G holds F * a is closed
let F be closed Subset of G; ::_thesis: for a being Element of G holds F * a is closed
let a be Element of G; ::_thesis: F * a is closed
F * a = (* a) .: F by Th17;
hence F * a is closed by TOPS_2:58; ::_thesis: verum
end;
theorem Th47: :: TOPGRP_1:47
for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds a * F is closed
proof
let G be BinContinuous TopGroup; ::_thesis: for F being closed Subset of G
for a being Element of G holds a * F is closed
let F be closed Subset of G; ::_thesis: for a being Element of G holds a * F is closed
let a be Element of G; ::_thesis: a * F is closed
a * F = (a *) .: F by Th16;
hence a * F is closed by TOPS_2:58; ::_thesis: verum
end;
registration
let G be BinContinuous TopGroup;
let F be closed Subset of G;
let a be Element of G;
clusterF * a -> closed ;
coherence
F * a is closed by Th46;
clustera * F -> closed ;
coherence
a * F is closed by Th47;
end;
theorem Th48: :: TOPGRP_1:48
for G being UnContinuous TopGroup
for F being closed Subset of G holds F " is closed
proof
let G be UnContinuous TopGroup; ::_thesis: for F being closed Subset of G holds F " is closed
let F be closed Subset of G; ::_thesis: F " is closed
F " = (inverse_op G) .: F by Th10;
hence F " is closed by TOPS_2:58; ::_thesis: verum
end;
registration
let G be UnContinuous TopGroup;
let F be closed Subset of G;
clusterF " -> closed ;
coherence
F " is closed by Th48;
end;
theorem Th49: :: TOPGRP_1:49
for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds O * a is open
proof
let G be BinContinuous TopGroup; ::_thesis: for O being open Subset of G
for a being Element of G holds O * a is open
let O be open Subset of G; ::_thesis: for a being Element of G holds O * a is open
let a be Element of G; ::_thesis: O * a is open
O * a = (* a) .: O by Th17;
hence O * a is open by Th25; ::_thesis: verum
end;
theorem Th50: :: TOPGRP_1:50
for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds a * O is open
proof
let G be BinContinuous TopGroup; ::_thesis: for O being open Subset of G
for a being Element of G holds a * O is open
let O be open Subset of G; ::_thesis: for a being Element of G holds a * O is open
let a be Element of G; ::_thesis: a * O is open
a * O = (a *) .: O by Th16;
hence a * O is open by Th25; ::_thesis: verum
end;
registration
let G be BinContinuous TopGroup;
let A be open Subset of G;
let a be Element of G;
clusterA * a -> open ;
coherence
A * a is open by Th49;
clustera * A -> open ;
coherence
a * A is open by Th50;
end;
theorem Th51: :: TOPGRP_1:51
for G being UnContinuous TopGroup
for O being open Subset of G holds O " is open
proof
let G be UnContinuous TopGroup; ::_thesis: for O being open Subset of G holds O " is open
let O be open Subset of G; ::_thesis: O " is open
O " = (inverse_op G) .: O by Th10;
hence O " is open by Th25; ::_thesis: verum
end;
registration
let G be UnContinuous TopGroup;
let A be open Subset of G;
clusterA " -> open ;
coherence
A " is open by Th51;
end;
theorem Th52: :: TOPGRP_1:52
for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
O * A is open
proof
let G be BinContinuous TopGroup; ::_thesis: for A, O being Subset of G st O is open holds
O * A is open
let A, O be Subset of G; ::_thesis: ( O is open implies O * A is open )
assume A1: O is open ; ::_thesis: O * A is open
Int (O * A) = O * A
proof
thus Int (O * A) c= O * A by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: O * A c= Int (O * A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O * A or x in Int (O * A) )
assume x in O * A ; ::_thesis: x in Int (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: O * a c= O * A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O * a or q in O * A )
assume q in O * a ; ::_thesis: q in O * A
then ex h being Element of G st
( q = h * a & h in O ) by GROUP_2:28;
hence q in O * A by A3; ::_thesis: verum
end;
x in O * a by A2, GROUP_2:28;
hence x in Int (O * A) by A1, A4, TOPS_1:22; ::_thesis: verum
end;
hence O * A is open ; ::_thesis: verum
end;
theorem Th53: :: TOPGRP_1:53
for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
A * O is open
proof
let G be BinContinuous TopGroup; ::_thesis: for A, O being Subset of G st O is open holds
A * O is open
let A, O be Subset of G; ::_thesis: ( O is open implies A * O is open )
assume A1: O is open ; ::_thesis: A * O is open
Int (A * O) = A * O
proof
thus Int (A * O) c= A * O by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: A * O c= Int (A * O)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * O or x in Int (A * O) )
assume x in A * O ; ::_thesis: x in Int (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: a * O c= A * O
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in a * O or q in A * O )
assume q in a * O ; ::_thesis: q in A * O
then ex h being Element of G st
( q = a * h & h in O ) by GROUP_2:27;
hence q in A * O by A3; ::_thesis: verum
end;
x in a * O by A2, A4, GROUP_2:27;
hence x in Int (A * O) by A1, A5, TOPS_1:22; ::_thesis: verum
end;
hence A * O is open ; ::_thesis: verum
end;
registration
let G be BinContinuous TopGroup;
let A be open Subset of G;
let B be Subset of G;
clusterA * B -> open ;
coherence
A * B is open by Th52;
clusterB * A -> open ;
coherence
B * A is open by Th53;
end;
theorem Th54: :: TOPGRP_1:54
for G being UnContinuous TopGroup
for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "
proof
let G be UnContinuous TopGroup; ::_thesis: for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "
let a be Point of G; ::_thesis: for A being a_neighborhood of a holds A " is a_neighborhood of a "
let A be a_neighborhood of a; ::_thesis: A " is 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, Th9;
hence a " in Int (A ") by A1, TOPS_1:22; :: according to CONNSP_2:def_1 ::_thesis: verum
end;
theorem Th55: :: TOPGRP_1:55
for G being TopologicalGroup
for a being Point of G
for 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; ::_thesis: for a being Point of G
for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A
let a be Point of G; ::_thesis: for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A
let A be a_neighborhood of a * (a "); ::_thesis: ex B being open a_neighborhood of a st B * (B ") c= A
consider X, Y being open a_neighborhood of a such that
A1: X * (Y ") c= A by Th41;
reconsider B = X /\ Y as open a_neighborhood of a by CONNSP_2:2;
take B ; ::_thesis: B * (B ") c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * (B ") or x in A )
assume x in B * (B ") ; ::_thesis: x in A
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 x in A by A1; ::_thesis: verum
end;
theorem Th56: :: TOPGRP_1:56
for G being UnContinuous TopGroup
for A being dense Subset of G holds A " is dense
proof
let G be UnContinuous TopGroup; ::_thesis: for A being dense Subset of G holds A " is dense
let A be dense Subset of G; ::_thesis: A " is dense
(inverse_op G) " A = A " by Th11;
hence A " is dense by Th29; ::_thesis: verum
end;
registration
let G be UnContinuous TopGroup;
let A be dense Subset of G;
clusterA " -> dense ;
coherence
A " is dense by Th56;
end;
theorem Th57: :: TOPGRP_1:57
for G being BinContinuous TopGroup
for A being dense Subset of G
for a being Point of G holds a * A is dense
proof
let G be BinContinuous TopGroup; ::_thesis: for A being dense Subset of G
for a being Point of G holds a * A is dense
let A be dense Subset of G; ::_thesis: for a being Point of G holds a * A is dense
let a be Point of G; ::_thesis: a * A is dense
(a *) .: A = a * A by Th16;
hence a * A is dense by Th28; ::_thesis: verum
end;
theorem Th58: :: TOPGRP_1:58
for G being BinContinuous TopGroup
for A being dense Subset of G
for a being Point of G holds A * a is dense
proof
let G be BinContinuous TopGroup; ::_thesis: for A being dense Subset of G
for a being Point of G holds A * a is dense
let A be dense Subset of G; ::_thesis: for a being Point of G holds A * a is dense
let a be Point of G; ::_thesis: A * a is dense
(* a) .: A = A * a by Th17;
hence A * a is dense by Th28; ::_thesis: verum
end;
registration
let G be BinContinuous TopGroup;
let A be dense Subset of G;
let a be Point of G;
clusterA * a -> dense ;
coherence
A * a is dense by Th58;
clustera * A -> dense ;
coherence
a * A is dense by Th57;
end;
theorem :: TOPGRP_1:59
for G being TopologicalGroup
for B being Basis of 1_ G
for 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; ::_thesis: for B being Basis of 1_ G
for 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
let B be Basis of 1_ G; ::_thesis: for 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
let M be dense Subset of G; ::_thesis: { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
set Z = { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ;
A1: { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= the topology of G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in the topology of G )
assume a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; ::_thesis: a in the topology of G
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 = V as Subset of G ;
V is open by A3, YELLOW_8:12;
hence a in the topology of G by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
A4: for W being Subset of G st W is open holds
for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & 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; ::_thesis: ( W is open implies for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) )
assume A6: W is open ; ::_thesis: for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )
let a be Point of G; ::_thesis: ( a in W implies ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) )
assume A7: a in W ; ::_thesis: ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= 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 Th55;
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 set such that
A11: d in (a * (M ")) /\ E by XBOOLE_0:4;
reconsider d = d as Point of G by A11;
take I = E * ((d ") * a); ::_thesis: ( I in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in I & I c= W )
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 { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } by A9; ::_thesis: ( a in I & I c= W )
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not q in E * (d ") or q in V * (V ") )
assume q in E * (d ") ; ::_thesis: q in V * (V ")
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 q in V * (V ") by A10, A16; ::_thesis: verum
end;
then E * (d ") c= W * (a ") by A8, XBOOLE_1:1;
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; ::_thesis: I c= W
(W * (a ")) * a = W * ((a ") * a) by GROUP_2:34
.= W * (1_ G) by GROUP_1:def_5
.= W by GROUP_2:37 ;
hence I c= W by A17, GROUP_2:34; ::_thesis: verum
end;
{ (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= bool the carrier of G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in bool the carrier of G )
assume a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; ::_thesis: a in bool the carrier of G
then ex V being Subset of G ex x being Point of G st
( a = V * x & V in B & x in M ) ;
hence a in bool the carrier of G ; ::_thesis: verum
end;
hence { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G by A1, A4, YELLOW_9:32; ::_thesis: verum
end;
theorem Th60: :: TOPGRP_1:60
for G being TopologicalGroup holds G is regular
proof
let G be TopologicalGroup; ::_thesis: G is regular
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 1_ G ; ::_thesis: for A being Subset of G st A is open & 1_ G in A holds
ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A )
let A be Subset of G; ::_thesis: ( A is open & 1_ G in A implies ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A ) )
assume ( A is open & 1_ G in A ) ; ::_thesis: ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A )
then 1_ G in Int A by TOPS_1:23;
then A1: A is a_neighborhood of 1_ G by CONNSP_2:def_1;
1_ G = (1_ G) * ((1_ G) ") by GROUP_1:def_5;
then consider C being open a_neighborhood of 1_ G, B being open a_neighborhood of (1_ G) " such that
A2: C * B c= A by A1, Th37;
((1_ G) ") " = 1_ G ;
then B " is a_neighborhood of 1_ G by Th54;
then reconsider W = C /\ (B ") as a_neighborhood of 1_ G by CONNSP_2:2;
W c= B " by XBOOLE_1:17;
then W " c= (B ") " by Th9;
then C * (W ") c= C * B by Th4;
then A3: C * (W ") c= A by A2, XBOOLE_1:1;
take W ; ::_thesis: ( 1_ G in W & W is open & Cl W c= A )
Int W = W by TOPS_1:23;
hence A4: ( 1_ G in W & W is open ) by CONNSP_2:def_1; ::_thesis: Cl W c= A
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Cl W or p in A )
assume A5: p in Cl W ; ::_thesis: p in A
then reconsider r = p as Point of G ;
r = r * (1_ G) 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 set 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 = 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 * (1_ G) 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 p in A by A3; ::_thesis: verum
end;
hence G is regular by Th36; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like Group-like associative UnContinuous BinContinuous -> regular for TopGrStr ;
coherence
for b1 being TopologicalGroup holds b1 is regular by Th60;
end;
theorem :: TOPGRP_1:61
for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism by Lm2;