:: The Definition and Basic Properties of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received September 7, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: TOPGRP_1:1
theorem Th2: :: TOPGRP_1:2
theorem :: TOPGRP_1:3
theorem Th4: :: TOPGRP_1:4
theorem Th5: :: TOPGRP_1:5
theorem :: TOPGRP_1:6
theorem Th7: :: TOPGRP_1:7
theorem Th8: :: TOPGRP_1:8
theorem Th9: :: TOPGRP_1:9
theorem Th10: :: TOPGRP_1:10
theorem Th11: :: TOPGRP_1:11
theorem Th12: :: TOPGRP_1:12
theorem Th13: :: TOPGRP_1:13
theorem Th14: :: TOPGRP_1:14
theorem Th15: :: TOPGRP_1:15
:: deftheorem Def1 defines * TOPGRP_1:def 1 :
:: deftheorem Def2 defines * TOPGRP_1:def 2 :
theorem Th16: :: TOPGRP_1:16
theorem Th17: :: TOPGRP_1:17
theorem Th18: :: TOPGRP_1:18
theorem Th19: :: TOPGRP_1:19
theorem Th20: :: TOPGRP_1:20
theorem Th21: :: TOPGRP_1:21
theorem :: TOPGRP_1:22
theorem :: TOPGRP_1:23
theorem :: TOPGRP_1:24
theorem Th25: :: TOPGRP_1:25
theorem :: TOPGRP_1:26
theorem :: TOPGRP_1:27
theorem Th28: :: TOPGRP_1:28
theorem Th29: :: TOPGRP_1:29
:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :
:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def 4 :
theorem Th30: :: TOPGRP_1:30
Lm1:
for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism
theorem Th31: :: TOPGRP_1:31
:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def 5 :
theorem :: TOPGRP_1:32
theorem Th33: :: TOPGRP_1:33
theorem :: TOPGRP_1:34
:: deftheorem Def6 defines homogeneous TOPGRP_1:def 6 :
theorem :: TOPGRP_1:35
theorem Th36: :: TOPGRP_1:36
:: deftheorem Def7 defines UnContinuous TOPGRP_1:def 7 :
:: deftheorem Def8 defines BinContinuous TOPGRP_1:def 8 :
theorem Th37: :: TOPGRP_1:37
theorem Th38: :: TOPGRP_1:38
theorem Th39: :: TOPGRP_1:39
theorem Th40: :: TOPGRP_1:40
theorem Th41: :: TOPGRP_1:41
theorem :: TOPGRP_1:42
theorem Th43: :: TOPGRP_1:43
theorem Th44: :: TOPGRP_1:44
theorem Th45: :: TOPGRP_1:45
theorem Th46: :: TOPGRP_1:46
theorem Th47: :: TOPGRP_1:47
theorem Th48: :: TOPGRP_1:48
theorem Th49: :: TOPGRP_1:49
theorem Th50: :: TOPGRP_1:50
theorem Th51: :: TOPGRP_1:51
theorem Th52: :: TOPGRP_1:52
theorem Th53: :: TOPGRP_1:53
theorem Th54: :: TOPGRP_1:54
theorem Th55: :: TOPGRP_1:55
theorem Th56: :: TOPGRP_1:56
theorem Th57: :: TOPGRP_1:57
theorem Th58: :: TOPGRP_1:58
theorem :: TOPGRP_1:59
theorem Th60: :: TOPGRP_1:60
theorem :: TOPGRP_1:61