:: TOPGRP_1 semantic presentation

registration

let c₁ be set ;
cluster one-to-one onto M4(a₁,a₁);
existence

proof end;

end;

theorem Th1: :: TOPGRP_1:1

for b₁ being 1-sorted holds rng (id b₁) = [#] b₁

proof end;

registration

let c₁ be non empty 1-sorted ;
cluster (id a₁) /" -> one-to-one ;
coherence

proof end;

end;

theorem Th2: :: TOPGRP_1:2

for b₁ being non empty 1-sorted holds (id b₁) /" = id b₁

proof end;

theorem Th3: :: TOPGRP_1:3

for b₁ being non empty 1-sorted
for b₂ being Subset of b₁ holds (id b₁) " b₂ = b₂

proof end;

registration

let c₁ be 1-sorted ;
cluster one-to-one onto M4(the carrier of a₁,the carrier of a₁);
existence

proof end;

end;

theorem Th4: :: TOPGRP_1:4

for b₁ being non empty HGrStr
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
b₂ * b₄ c= b₃ * b₅

proof end;

theorem Th5: :: TOPGRP_1:5

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₂ c= b₃ holds
b₂ * b₄ c= b₃ * b₄

proof end;

theorem Th6: :: TOPGRP_1:6

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ st b₂ c= b₃ holds
b₄ * b₂ c= b₄ * b₃

proof end;

theorem Th7: :: TOPGRP_1:7

for b₁ being Group
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in b₂ " iff b₃ " in b₂ )

proof end;

theorem Th8: :: TOPGRP_1:8

for b₁ being Group
for b₂ being Subset of b₁ holds (b₂ " ) " = b₂

proof end;

theorem Th9: :: TOPGRP_1:9

for b₁ being Group
for b₂, b₃ being Subset of b₁ holds
( b₂ c= b₃ iff b₂ " c= b₃ " )

proof end;

theorem Th10: :: TOPGRP_1:10

for b₁ being Group
for b₂ being Subset of b₁ holds (inverse_op b₁) .: b₂ = b₂ "

proof end;

theorem Th11: :: TOPGRP_1:11

for b₁ being Group
for b₂ being Subset of b₁ holds (inverse_op b₁) " b₂ = b₂ "

proof end;

theorem Th12: :: TOPGRP_1:12

for b₁ being Group holds inverse_op b₁ is one-to-one

proof end;

theorem Th13: :: TOPGRP_1:13

for b₁ being Group holds rng (inverse_op b₁) = the carrier of b₁

proof end;

registration

let c₁ be Group;
cluster inverse_op a₁ -> one-to-one onto ;
coherence

proof end;

end;

theorem Th14: :: TOPGRP_1:14

for b₁ being Group holds (inverse_op b₁) " = inverse_op b₁

proof end;

theorem Th15: :: TOPGRP_1:15

for b₁ being non empty HGrStr
for b₂, b₃ being Subset of b₁ holds the mult of b₁ .: [:b₂,b₃:] = b₂ * b₃

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be Element of c₁;
func c₂ * -> Function of a₁,a₁ means :Def1: :: TOPGRP_1:def 1
for b₁ being Element of a₁ holds a₃ . b₁ = a₂ * b₁;
existence

proof end;

uniqueness

proof end;

func * c₂ -> Function of a₁,a₁ means :Def2: :: TOPGRP_1:def 2
for b₁ being Element of a₁ holds a₃ . b₁ = b₁ * a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines * TOPGRP_1:def 1 :

:: deftheorem Def2 defines * TOPGRP_1:def 2 :

registration

let c₁ be Group;
let c₂ be Element of c₁;
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 b₁ being non empty HGrStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds (b₃ * ) .: b₂ = b₃ * b₂

proof end;

theorem Th17: :: TOPGRP_1:17

for b₁ being non empty HGrStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds (* b₃) .: b₂ = b₂ * b₃

proof end;

theorem Th18: :: TOPGRP_1:18

for b₁ being Group
for b₂ being Element of b₁ holds (b₂ * ) /" = (b₂ " ) *

proof end;

theorem Th19: :: TOPGRP_1:19

for b₁ being Group
for b₂ being Element of b₁ holds (* b₂) /" = * (b₂ " )

proof end;

registration

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

end;

theorem Th20: :: TOPGRP_1:20

for b₁ being non empty TopStruct holds id b₁ is_homeomorphism

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster -> non empty a_neighborhood of a₂;
coherence

proof end;

end;

theorem Th21: :: TOPGRP_1:21

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds [#] b₁ is a_neighborhood of b₂

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster non empty open a_neighborhood of a₂;
existence

proof end;

end;

theorem Th22: :: TOPGRP_1:22

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is open holds
for b₄ being Point of b₁
for b₅ being a_neighborhood of b₄ ex b₆ being open a_neighborhood of b₃ . b₄ st b₆ c= b₃ .: b₅

proof end;

theorem Th23: :: TOPGRP_1:23

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st ( for b₄ being Point of b₁
for b₅ being open a_neighborhood of b₄ ex b₆ being a_neighborhood of b₃ . b₄ st b₆ c= b₃ .: b₅ ) holds
b₃ is open

proof end;

theorem Th24: :: TOPGRP_1:24

for b₁, b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ holds
( b₃ is_homeomorphism iff ( dom b₃ = [#] b₁ & rng b₃ = [#] b₂ & b₃ is one-to-one & ( for b₄ being Subset of b₂ holds
( b₄ is closed iff b₃ " b₄ is closed ) ) ) )

proof end;

theorem Th25: :: TOPGRP_1:25

for b₁, b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ holds
( b₃ is_homeomorphism iff ( dom b₃ = [#] b₁ & rng b₃ = [#] b₂ & b₃ is one-to-one & ( for b₄ being Subset of b₁ holds
( b₄ is open iff b₃ .: b₄ is open ) ) ) )

proof end;

theorem Th26: :: TOPGRP_1:26

proof end;

theorem Th27: :: TOPGRP_1:27

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is continuous iff for b₄ being Subset of b₂ holds b₃ " (Int b₄) c= Int (b₃ " b₄) )

proof end;

registration

let c₁ be non empty TopSpace;
cluster non empty dense Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th28: :: TOPGRP_1:28

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being dense Subset of b₁ st b₃ is_homeomorphism holds
b₃ .: b₄ is dense

proof end;

theorem Th29: :: TOPGRP_1:29

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being dense Subset of b₂ st b₃ is_homeomorphism holds
b₃ " b₄ is dense

proof end;

registration

let c₁, c₂ be non empty TopStruct ;
cluster being_homeomorphism -> one-to-one onto continuous open M4(the carrier of a₁,the carrier of a₂);
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

end;

definition

let c₁ be non empty TopStruct ;
mode Homeomorphism of c₁ -> Function of a₁,a₁ means :Def3: :: TOPGRP_1:def 3
a₂ is_homeomorphism ;
existence

proof end;

end;

:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :

definition

let c₁ be non empty TopStruct ;
redefine func id as id c₁ -> Homeomorphism of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
cluster -> being_homeomorphism Homeomorphism of a₁;
coherence by Def3;

end;

theorem Th30: :: TOPGRP_1:30

for b₁ being non empty TopStruct
for b₂ being Homeomorphism of b₁ holds b₂ /" is Homeomorphism of b₁

proof end;

theorem Th31: :: TOPGRP_1:31

for b₁ being non empty TopStruct
for b₂, b₃ being Homeomorphism of b₁ holds b₂ * b₃ is Homeomorphism of b₁

proof end;

definition

let c₁ be non empty TopStruct ;
func HomeoGroup c₁ -> strict HGrStr means :Def4: :: TOPGRP_1:def 4
for b₁ being set holds
( ( b₁ in the carrier of a₂ implies b₁ is Homeomorphism of a₁ ) & ( b₁ is Homeomorphism of a₁ implies b₁ in the carrier of a₂ ) & ( for b₂, b₃ being Homeomorphism of a₁ holds the mult of a₂ . b₂,b₃ = b₃ * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines HomeoGroup TOPGRP_1:def 4 :

registration

let c₁ be non empty TopStruct ;
cluster HomeoGroup a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th32: :: TOPGRP_1:32

for b₁ being non empty TopStruct
for b₂, b₃ being Homeomorphism of b₁
for b₄, b₅ being Element of (HomeoGroup b₁) st b₂ = b₄ & b₃ = b₅ holds
b₄ * b₅ = b₃ * b₂ by Def4;

registration

let c₁ be non empty TopStruct ;
cluster HomeoGroup a₁ -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th33: :: TOPGRP_1:33

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

proof end;

theorem Th34: :: TOPGRP_1:34

for b₁ being non empty TopStruct
for b₂ being Homeomorphism of b₁
for b₃ being Element of (HomeoGroup b₁) st b₂ = b₃ holds
b₃ " = b₂ /"

proof end;

definition

let c₁ be non empty TopStruct ;
attr a₁ is homogeneous means :Def5: :: TOPGRP_1:def 5
for b₁, b₂ being Point of a₁ ex b₃ being Homeomorphism of a₁ st b₃ . b₁ = b₂;

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 Th35: :: TOPGRP_1:35

for b₁ being non empty homogeneous TopSpace st ex b₂ being Point of b₁ st {b₂} is closed holds
b₁ is_T1

proof end;

theorem Th36: :: TOPGRP_1:36

for b₁ being non empty homogeneous TopSpace st ex b₂ being Point of b₁ st
for b₃ being Subset of b₁ st b₃ is open & b₂ in b₃ holds
ex b₄ being Subset of b₁ st
( b₂ in b₄ & b₄ is open & Cl b₄ c= b₃ ) holds
b₁ is_T3

proof end;

definition

attr a₁ is strict;
struct TopGrStr -> HGrStr , TopStruct ;
aggr TopGrStr(# carrier, mult, topology #) -> TopGrStr ;

end;

registration

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
let c₃ be Subset-Family of c₁;
cluster TopGrStr(# a₁,a₂,a₃ #) -> non empty ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be BinOp of {c₁};
let c₃ be Subset-Family of {c₁};
cluster TopGrStr(# {a₁},a₂,a₃ #) -> 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 c₁ 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 c₁ be non empty Group-like associative TopGrStr ;
redefine func inverse_op as inverse_op c₁ -> Function of a₁,a₁;
coherence ;

end;

definition

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

end;

:: deftheorem Def6 defines UnContinuous TOPGRP_1:def 6 :

definition

let c₁ be TopSpace-like TopGrStr ;
attr a₁ is BinContinuous means :Def7: :: TOPGRP_1:def 7
for b₁ being Function of [:a₁,a₁:],a₁ st b₁ = the mult of a₁ holds
b₁ 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 b₁ being non empty TopSpace-like BinContinuous TopGrStr
for b₂, b₃ being Element of b₁
for b₄ being a_neighborhood of b₂ * b₃ ex b₅ being open a_neighborhood of b₂ex b₆ being open a_neighborhood of b₃ st b₅ * b₆ c= b₄

proof end;

theorem Th38: :: TOPGRP_1:38

for b₁ being non empty TopSpace-like TopGrStr st ( for b₂, b₃ being Element of b₁
for b₄ being a_neighborhood of b₂ * b₃ ex b₅ being a_neighborhood of b₂ex b₆ being a_neighborhood of b₃ st b₅ * b₆ c= b₄ ) holds
b₁ is BinContinuous

proof end;

theorem Th39: :: TOPGRP_1:39

for b₁ being UnContinuous TopGroup
for b₂ being Element of b₁
for b₃ being a_neighborhood of b₂ " ex b₄ being open a_neighborhood of b₂ st b₄ " c= b₃

proof end;

theorem Th40: :: TOPGRP_1:40

for b₁ being TopGroup st ( for b₂ being Element of b₁
for b₃ being a_neighborhood of b₂ " ex b₄ being a_neighborhood of b₂ st b₄ " c= b₃ ) holds
b₁ is UnContinuous

proof end;

theorem Th41: :: TOPGRP_1:41

for b₁ being TopologicalGroup
for b₂, b₃ being Element of b₁
for b₄ being a_neighborhood of b₂ * (b₃ " ) ex b₅ being open a_neighborhood of b₂ex b₆ being open a_neighborhood of b₃ st b₅ * (b₆ " ) c= b₄

proof end;

theorem Th42: :: TOPGRP_1:42

for b₁ being TopGroup st ( for b₂, b₃ being Element of b₁
for b₄ being a_neighborhood of b₂ * (b₃ " ) ex b₅ being a_neighborhood of b₂ex b₆ being a_neighborhood of b₃ st b₅ * (b₆ " ) c= b₄ ) holds
b₁ is TopologicalGroup

proof end;

registration

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

proof end;

cluster * a₂ -> continuous ;
coherence

proof end;

end;

theorem Th43: :: TOPGRP_1:43

for b₁ being BinContinuous TopGroup
for b₂ being Element of b₁ holds b₂ * is Homeomorphism of b₁

proof end;

theorem Th44: :: TOPGRP_1:44

for b₁ being BinContinuous TopGroup
for b₂ being Element of b₁ holds * b₂ is Homeomorphism of b₁

proof end;

definition

let c₁ be BinContinuous TopGroup;
let c₂ be Element of c₁;
redefine func * as c₂ * -> Homeomorphism of a₁;
coherence by Th43;
redefine func * as * c₂ -> Homeomorphism of a₁;
coherence by Th44;

end;

theorem Th45: :: TOPGRP_1:45

for b₁ being UnContinuous TopGroup holds inverse_op b₁ is Homeomorphism of b₁

proof end;

definition

let c₁ be UnContinuous TopGroup;
redefine func inverse_op as inverse_op c₁ -> Homeomorphism of a₁;
coherence by Th45;

end;

registration

cluster BinContinuous -> homogeneous TopGrStr ;
coherence

proof end;

end;

theorem Th46: :: TOPGRP_1:46

for b₁ being BinContinuous TopGroup
for b₂ being closed Subset of b₁
for b₃ being Element of b₁ holds b₂ * b₃ is closed

proof end;

theorem Th47: :: TOPGRP_1:47

for b₁ being BinContinuous TopGroup
for b₂ being closed Subset of b₁
for b₃ being Element of b₁ holds b₃ * b₂ is closed

proof end;

registration

let c₁ be BinContinuous TopGroup;
let c₂ be closed Subset of c₁;
let c₃ be Element of c₁;
cluster a₂ * a₃ -> closed ;
coherence by Th46;
cluster a₃ * a₂ -> closed ;
coherence by Th47;

end;

theorem Th48: :: TOPGRP_1:48

for b₁ being UnContinuous TopGroup
for b₂ being closed Subset of b₁ holds b₂ " is closed

proof end;

registration

let c₁ be UnContinuous TopGroup;
let c₂ be closed Subset of c₁;
cluster a₂ " -> closed ;
coherence by Th48;

end;

theorem Th49: :: TOPGRP_1:49

for b₁ being BinContinuous TopGroup
for b₂ being open Subset of b₁
for b₃ being Element of b₁ holds b₂ * b₃ is open

proof end;

theorem Th50: :: TOPGRP_1:50

for b₁ being BinContinuous TopGroup
for b₂ being open Subset of b₁
for b₃ being Element of b₁ holds b₃ * b₂ is open

proof end;

registration

let c₁ be BinContinuous TopGroup;
let c₂ be open Subset of c₁;
let c₃ be Element of c₁;
cluster a₂ * a₃ -> open ;
coherence by Th49;
cluster a₃ * a₂ -> open ;
coherence by Th50;

end;

theorem Th51: :: TOPGRP_1:51

for b₁ being UnContinuous TopGroup
for b₂ being open Subset of b₁ holds b₂ " is open

proof end;

registration

let c₁ be UnContinuous TopGroup;
let c₂ be open Subset of c₁;
cluster a₂ " -> open ;
coherence by Th51;

end;

theorem Th52: :: TOPGRP_1:52

for b₁ being BinContinuous TopGroup
for b₂, b₃ being Subset of b₁ st b₃ is open holds
b₃ * b₂ is open

proof end;

theorem Th53: :: TOPGRP_1:53

for b₁ being BinContinuous TopGroup
for b₂, b₃ being Subset of b₁ st b₃ is open holds
b₂ * b₃ is open

proof end;

registration

let c₁ be BinContinuous TopGroup;
let c₂ be open Subset of c₁;
let c₃ be Subset of c₁;
cluster a₂ * a₃ -> open ;
coherence by Th52;
cluster a₃ * a₂ -> open ;
coherence by Th53;

end;

theorem Th54: :: TOPGRP_1:54

for b₁ being UnContinuous TopGroup
for b₂ being Point of b₁
for b₃ being a_neighborhood of b₂ holds b₃ " is a_neighborhood of b₂ "

proof end;

theorem Th55: :: TOPGRP_1:55

for b₁ being TopologicalGroup
for b₂ being Point of b₁
for b₃ being a_neighborhood of b₂ * (b₂ " ) ex b₄ being open a_neighborhood of b₂ st b₄ * (b₄ " ) c= b₃

proof end;

theorem Th56: :: TOPGRP_1:56

for b₁ being UnContinuous TopGroup
for b₂ being dense Subset of b₁ holds b₂ " is dense

proof end;

registration

let c₁ be UnContinuous TopGroup;
let c₂ be dense Subset of c₁;
cluster a₂ " -> dense ;
coherence by Th56;

end;

theorem Th57: :: TOPGRP_1:57

for b₁ being BinContinuous TopGroup
for b₂ being dense Subset of b₁
for b₃ being Point of b₁ holds b₃ * b₂ is dense

proof end;

theorem Th58: :: TOPGRP_1:58

for b₁ being BinContinuous TopGroup
for b₂ being dense Subset of b₁
for b₃ being Point of b₁ holds b₂ * b₃ is dense

proof end;

registration

let c₁ be BinContinuous TopGroup;
let c₂ be dense Subset of c₁;
let c₃ be Point of c₁;
cluster a₂ * a₃ -> dense ;
coherence by Th58;
cluster a₃ * a₂ -> dense ;
coherence by Th57;

end;

theorem Th59: :: TOPGRP_1:59

for b₁ being TopologicalGroup
for b₂ being Basis of 1. b₁
for b₃ being dense Subset of b₁ holds { (b₄ * b₅) where B is Subset of b₁, B is Point of b₁ : ( b₄ in b₂ & b₅ in b₃ ) } is Basis of b₁

proof end;

theorem Th60: :: TOPGRP_1:60

for b₁ being TopologicalGroup holds b₁ is_T3

proof end;

registration

cluster -> being_T3 homogeneous TopGrStr ;
coherence by Th60;

end;