let G be non empty HGrStr ;
let a be Element of G;
func a * -> Function of G,G means :Def1: :: TOPGRP_1:def 1
for x being Element of G holds it . x = a * x;
existence

proof end;

uniqueness

proof 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines * TOPGRP_1:def 1 :

:: deftheorem Def2 defines * TOPGRP_1:def 2 :

registration

let G be Group;
let a be Element of G;
cluster a * -> one-to-one onto ;
coherence

proof end;

cluster * a -> one-to-one onto ;
coherence

proof end;

end;

theorem Th16: :: TOPGRP_1:16

for H being non empty HGrStr
for P being Subset of H
for h being Element of H holds (h * ) .: P = h * P

proof end;

theorem Th17: :: TOPGRP_1:17

for H being non empty HGrStr
for P being Subset of H
for h being Element of H holds (* h) .: P = P * h

proof end;

theorem Th18: :: TOPGRP_1:18

for G being Group
for a being Element of G holds (a * ) /" = (a " ) *

proof end;

theorem Th19: :: TOPGRP_1:19

for G being Group
for a being Element of G holds (* a) /" = * (a " )

proof end;

registration

let T be non empty TopStruct ;
cluster (id T) /" -> one-to-one continuous ;
coherence by Th2;

end;

theorem Th20: :: TOPGRP_1:20

for T being non empty TopStruct holds id T is_homeomorphism

proof end;

registration

let T be non empty TopSpace;
let p be Point of T;
cluster -> non empty a_neighborhood of p;
coherence

proof 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 end;

registration

let T be non empty TopSpace;
let p be Point of T;
cluster non empty open a_neighborhood of p;
existence

proof 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 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 end;

theorem :: TOPGRP_1:24

for S, T being non empty TopStruct
for f being Function of S,T holds
( f is_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f " P is closed ) ) ) )

proof end;

theorem Th25: :: TOPGRP_1:25

for S, T being non empty TopStruct
for f being Function of S,T holds
( f is_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of S holds
( P is open iff f .: P is open ) ) ) )

proof end;

theorem :: TOPGRP_1:26

for S, T being non empty TopStruct
for f being Function of S,T holds
( f is_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( P is open iff f " P is open ) ) ) )

proof 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 end;

registration

let T be non empty TopSpace;
cluster non empty dense Element of bool the carrier of T;
existence

proof 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_homeomorphism holds
f .: A is dense

proof 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_homeomorphism holds
f " A is dense

proof end;

registration

let S, T be non empty TopStruct ;
cluster being_homeomorphism -> one-to-one onto continuous open M4(the carrier of S,the carrier of T);
coherence

proof end;

end;

registration

let T be non empty TopStruct ;
cluster one-to-one onto continuous being_homeomorphism open M4(the carrier of T,the carrier of T);
existence

proof end;

end;

registration

let T be non empty TopStruct ;
let f be being_homeomorphism Function of T,T;
cluster f /" -> one-to-one onto continuous being_homeomorphism open ;
coherence by TOPS_2:70;

end;

definition

let T be non empty TopStruct ;
mode Homeomorphism of T -> Function of T,T means :Def3: :: TOPGRP_1:def 3
it is_homeomorphism ;
existence

proof end;

end;

:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :

definition

let T be non empty TopStruct ;
:: original: id
redefine func id T -> Homeomorphism of T;
coherence

proof end;

end;

registration

let T be non empty TopStruct ;
cluster -> being_homeomorphism Homeomorphism of T;
coherence by Def3;

end;

theorem Th30: :: TOPGRP_1:30

for T being non empty TopStruct
for f being Homeomorphism of T holds f /" is Homeomorphism of T

proof end;

theorem Th31: :: TOPGRP_1:31

for T being non empty TopStruct
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T

proof end;

definition

let T be non empty TopStruct ;
func HomeoGroup T -> strict HGrStr means :Def4: :: TOPGRP_1:def 4
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 mult of it . f,g = g * f ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines HomeoGroup TOPGRP_1:def 4 :

registration

let T be non empty TopStruct ;
cluster HomeoGroup T -> non empty strict ;
coherence

proof end;

end;

theorem :: TOPGRP_1:32

for T being non empty 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 Def4;

registration

let T be non empty TopStruct ;
cluster HomeoGroup T -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th33: :: TOPGRP_1:33

for T being non empty TopStruct holds id T = 1. (HomeoGroup T)

proof end;

theorem :: TOPGRP_1:34

for T being non empty TopStruct
for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"

proof end;

definition

let T be non empty TopStruct ;
attr T is homogeneous means :Def5: :: TOPGRP_1:def 5
for p, q being Point of T ex f being Homeomorphism of T st f . p = q;

end;

:: deftheorem Def5 defines homogeneous TOPGRP_1:def 5 :

registration

cluster non empty trivial -> non empty homogeneous TopStruct ;
coherence

proof end;

end;

registration

cluster non empty trivial strict homogeneous TopStruct ;
existence

proof 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_T1

proof 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_T3

proof end;

definition

attr c₁ is strict;
struct TopGrStr -> HGrStr , TopStruct ;
aggr TopGrStr(# carrier, mult, 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

proof end;

end;

registration

let x be set ;
let R be BinOp of {x};
let T be Subset-Family of {x};
cluster TopGrStr(# {x},R,T #) -> non empty trivial homogeneous ;
coherence

proof end;

end;

registration

cluster non empty trivial -> non empty Group-like associative commutative HGrStr ;
coherence

proof end;

end;

registration

let a be set ;
cluster 1TopSp {a} -> trivial homogeneous ;
coherence

proof end;

end;

registration

cluster non empty strict TopGrStr ;
existence

proof end;

end;

registration

cluster non empty Group-like associative commutative trivial TopSpace-like homogeneous strict TopGrStr ;
existence

proof end;

end;

definition

let G be non empty Group-like associative TopGrStr ;
:: original: inverse_op
redefine func inverse_op G -> Function of G,G;
coherence ;

end;

definition

let G be non empty Group-like associative TopGrStr ;
attr G is UnContinuous means :Def6: :: TOPGRP_1:def 6
inverse_op G is continuous;

end;

:: deftheorem Def6 defines UnContinuous TOPGRP_1:def 6 :

definition

let G be TopSpace-like TopGrStr ;
attr G is BinContinuous means :Def7: :: TOPGRP_1:def 7
for f being Function of [:G,G:],G st f = the mult of G holds
f is continuous;

end;

:: deftheorem Def7 defines BinContinuous TOPGRP_1:def 7 :

registration

cluster non empty Group-like associative commutative trivial TopSpace-like homogeneous strict UnContinuous BinContinuous TopGrStr ;
existence

proof end;

end;

definition

mode TopGroup is non empty Group-like associative TopSpace-like 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 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 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 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 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 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 end;

registration

let G be non empty TopSpace-like BinContinuous TopGrStr ;
let a be Element of G;
cluster a * -> continuous ;
coherence

proof end;

cluster * a -> continuous ;
coherence

proof 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 end;

theorem Th44: :: TOPGRP_1:44

for G being BinContinuous TopGroup
for a being Element of G holds * a is Homeomorphism of G

proof end;

definition

let G be BinContinuous TopGroup;
let a be Element of G;
:: original: *
redefine func a * -> Homeomorphism of G;
coherence by Th43;
:: original: *
redefine func * a -> Homeomorphism of G;
coherence by Th44;

end;

theorem Th45: :: TOPGRP_1:45

for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G

proof end;

definition

let G be UnContinuous TopGroup;
:: original: inverse_op
redefine func inverse_op G -> Homeomorphism of G;
coherence by Th45;

end;

registration

cluster BinContinuous -> homogeneous TopGrStr ;
coherence

proof 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 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 end;

registration

let G be BinContinuous TopGroup;
let F be closed Subset of G;
let a be Element of G;
cluster F * a -> closed ;
coherence by Th46;
cluster a * F -> closed ;
coherence 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 end;

registration

let G be UnContinuous TopGroup;
let F be closed Subset of G;
cluster F " -> closed ;
coherence 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 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 end;

registration

let G be BinContinuous TopGroup;
let A be open Subset of G;
let a be Element of G;
cluster A * a -> open ;
coherence by Th49;
cluster a * A -> open ;
coherence 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 end;

registration

let G be UnContinuous TopGroup;
let A be open Subset of G;
cluster A " -> open ;
coherence 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 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 end;

registration

let G be BinContinuous TopGroup;
let A be open Subset of G;
let B be Subset of G;
cluster A * B -> open ;
coherence by Th52;
cluster B * A -> open ;
coherence 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 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 end;

theorem Th56: :: TOPGRP_1:56

for G being UnContinuous TopGroup
for A being dense Subset of G holds A " is dense

proof end;

registration

let G be UnContinuous TopGroup;
let A be dense Subset of G;
cluster A " -> dense ;
coherence 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 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 end;

registration

let G be BinContinuous TopGroup;
let A be dense Subset of G;
let a be Point of G;
cluster A * a -> dense ;
coherence by Th58;
cluster a * A -> dense ;
coherence 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 end;

theorem Th60: :: TOPGRP_1:60

for G being TopologicalGroup holds G is_T3

proof end;

registration

cluster -> being_T3 homogeneous TopGrStr ;
coherence by Th60;

end;