:: The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 31, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: ISOMICHI:1
theorem Th2: :: ISOMICHI:2
:: deftheorem Def1 defines supercondensed ISOMICHI:def 1 :
:: deftheorem Def2 defines subcondensed ISOMICHI:def 2 :
theorem :: ISOMICHI:3
theorem Th4: :: ISOMICHI:4
:: deftheorem Def3 defines condensed ISOMICHI:def 3 :
theorem Th5: :: ISOMICHI:5
theorem :: ISOMICHI:6
theorem :: ISOMICHI:7
theorem Th8: :: ISOMICHI:8
theorem Th9: :: ISOMICHI:9
theorem Th10: :: ISOMICHI:10
theorem :: ISOMICHI:11
theorem :: ISOMICHI:12
canceled;
theorem :: ISOMICHI:13
canceled;
theorem :: ISOMICHI:14
theorem Th15: :: ISOMICHI:15
theorem Th16: :: ISOMICHI:16
theorem Th17: :: ISOMICHI:17
theorem :: ISOMICHI:18
theorem :: ISOMICHI:19
theorem :: ISOMICHI:20
theorem :: ISOMICHI:21
:: deftheorem defines Bound ISOMICHI:def 4 :
theorem :: ISOMICHI:22
theorem :: ISOMICHI:23
:: deftheorem defines Border ISOMICHI:def 5 :
theorem Th24: :: ISOMICHI:24
theorem Th25: :: ISOMICHI:25
theorem Th26: :: ISOMICHI:26
theorem :: ISOMICHI:27
theorem :: ISOMICHI:28
theorem :: ISOMICHI:29
theorem Th30: :: ISOMICHI:30
theorem :: ISOMICHI:31
theorem :: ISOMICHI:32
theorem :: ISOMICHI:33
canceled;
theorem :: ISOMICHI:34
canceled;
theorem Th35: :: ISOMICHI:35
theorem Th36: :: ISOMICHI:36
theorem Th37: :: ISOMICHI:37
Lm1:
for a, b being real number st a < b holds
[.a,b.] \/ {b} = [.a,b.]
theorem :: ISOMICHI:38
canceled;
theorem :: ISOMICHI:39
canceled;
theorem :: ISOMICHI:40
canceled;
theorem :: ISOMICHI:41
theorem :: ISOMICHI:42
canceled;
theorem :: ISOMICHI:43
canceled;
theorem Th44: :: ISOMICHI:44
theorem Th45: :: ISOMICHI:45
:: deftheorem Def6 defines 1st_class ISOMICHI:def 6 :
:: deftheorem Def7 defines 2nd_class ISOMICHI:def 7 :
:: deftheorem Def8 defines 3rd_class ISOMICHI:def 8 :
theorem :: ISOMICHI:46
theorem Th47: :: ISOMICHI:47
:: deftheorem Def9 defines with_1st_class_subsets ISOMICHI:def 9 :
:: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def 10 :
:: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def 11 :
theorem Th48: :: ISOMICHI:48
theorem Th49: :: ISOMICHI:49
theorem Th50: :: ISOMICHI:50
theorem Th51: :: ISOMICHI:51
theorem Th52: :: ISOMICHI:52
theorem Th53: :: ISOMICHI:53
theorem :: ISOMICHI:54