:: Topology of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 25, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: deftheorem Def1 defines is_parallel_to RUSUB_5:def 1 :
theorem :: RUSUB_5:1
theorem Th2: :: RUSUB_5:2
theorem Th3: :: RUSUB_5:3
:: deftheorem defines - RUSUB_5:def 2 :
theorem Th4: :: RUSUB_5:4
theorem :: RUSUB_5:5
theorem :: RUSUB_5:6
theorem :: RUSUB_5:7
theorem Th8: :: RUSUB_5:8
theorem Th9: :: RUSUB_5:9
theorem :: RUSUB_5:10
theorem :: RUSUB_5:11
theorem Th12: :: RUSUB_5:12
theorem Th13: :: RUSUB_5:13
theorem Th14: :: RUSUB_5:14
theorem Th15: :: RUSUB_5:15
theorem Th16: :: RUSUB_5:16
theorem Th17: :: RUSUB_5:17
theorem Th18: :: RUSUB_5:18
theorem Th19: :: RUSUB_5:19
theorem :: RUSUB_5:20
:: deftheorem Def3 defines Ort_Comp RUSUB_5:def 3 :
:: deftheorem Def4 defines Ort_Comp RUSUB_5:def 4 :
theorem :: RUSUB_5:21
theorem :: RUSUB_5:22
theorem :: RUSUB_5:23
theorem :: RUSUB_5:24
theorem Th25: :: RUSUB_5:25
theorem Th26: :: RUSUB_5:26
theorem Th27: :: RUSUB_5:27
theorem :: RUSUB_5:28
theorem Th29: :: RUSUB_5:29
theorem :: RUSUB_5:30
theorem :: RUSUB_5:31
theorem :: RUSUB_5:32
:: deftheorem Def5 defines Family_open_set RUSUB_5:def 5 :
theorem Th33: :: RUSUB_5:33
theorem Th34: :: RUSUB_5:34
theorem Th35: :: RUSUB_5:35
theorem :: RUSUB_5:36
theorem Th37: :: RUSUB_5:37
theorem Th38: :: RUSUB_5:38
theorem Th39: :: RUSUB_5:39
theorem Th40: :: RUSUB_5:40
theorem Th41: :: RUSUB_5:41
:: deftheorem defines TopUnitSpace RUSUB_5:def 6 :
theorem :: RUSUB_5:42
theorem :: RUSUB_5:43
theorem :: RUSUB_5:44
theorem :: RUSUB_5:45
theorem :: RUSUB_5:46
theorem :: RUSUB_5:47
theorem :: RUSUB_5:48
theorem :: RUSUB_5:49
theorem Th50: :: RUSUB_5:50
theorem :: RUSUB_5:51
theorem :: RUSUB_5:52
theorem Th53: :: RUSUB_5:53
theorem :: RUSUB_5:54