:: Suprema and Infima of Intervals of Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received June 26, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Def1 defines UpperBound XXREAL_2:def 1 :
:: deftheorem Def2 defines LowerBound XXREAL_2:def 2 :
:: deftheorem Def3 defines sup XXREAL_2:def 3 :
:: deftheorem Def4 defines inf XXREAL_2:def 4 :
:: deftheorem Def5 defines left_end XXREAL_2:def 5 :
:: deftheorem Def6 defines right_end XXREAL_2:def 6 :
theorem Th1: :: XXREAL_2:1
theorem Th2: :: XXREAL_2:2
Lm1:
for x being ext-real number holds sup {x} = x
Lm2:
for x being ext-real number holds inf {x} = x
theorem Th3: :: XXREAL_2:3
theorem Th3B: :: XXREAL_2:4
theorem Th4: :: XXREAL_2:5
theorem Th4B: :: XXREAL_2:6
theorem Th5: :: XXREAL_2:7
theorem Th5B: :: XXREAL_2:8
theorem Th6: :: XXREAL_2:9
theorem Th6B: :: XXREAL_2:10
:: deftheorem Def7 defines inf XXREAL_2:def 7 :
:: deftheorem Def7B defines sup XXREAL_2:def 8 :
theorem :: XXREAL_2:11
Lm3:
for x, y being ext-real number st x <= y holds
y is UpperBound of {x,y}
Lm4:
for x, y being ext-real number
for z being UpperBound of {x,y} holds y <= z
theorem :: XXREAL_2:12
theorem :: XXREAL_2:13
Lm3:
for y, x being ext-real number st y <= x holds
y is LowerBound of {x,y}
Lm4:
for x, y being ext-real number
for z being LowerBound of {x,y} holds z <= y
theorem :: XXREAL_2:14
:: deftheorem Def9 defines bounded_below XXREAL_2:def 9 :
:: deftheorem Def10 defines bounded_above XXREAL_2:def 10 :
:: deftheorem Def11 defines bounded XXREAL_2:def 11 :
theorem Th15: :: XXREAL_2:15
theorem Th16: :: XXREAL_2:16
theorem Th17: :: XXREAL_2:17
theorem Th18: :: XXREAL_2:18
theorem Th19: :: XXREAL_2:19
theorem Th20: :: XXREAL_2:20
theorem Th21: :: XXREAL_2:21
theorem Th22: :: XXREAL_2:22
theorem Th23: :: XXREAL_2:23
theorem Th24: :: XXREAL_2:24
theorem Th25: :: XXREAL_2:25
theorem Th26: :: XXREAL_2:26
theorem Th27: :: XXREAL_2:27
theorem Th28: :: XXREAL_2:28
theorem Th29: :: XXREAL_2:29
theorem Th30: :: XXREAL_2:30
theorem Th31: :: XXREAL_2:31
theorem Th32: :: XXREAL_2:32
theorem Th33: :: XXREAL_2:33
theorem Th34: :: XXREAL_2:34
theorem Th35: :: XXREAL_2:35
theorem TW1: :: XXREAL_2:36
theorem TW2: :: XXREAL_2:37
theorem TW3: :: XXREAL_2:38
theorem TW4: :: XXREAL_2:39
theorem Th40: :: XXREAL_2:40
theorem :: XXREAL_2:41
theorem :: XXREAL_2:42
theorem Th43: :: XXREAL_2:43
theorem Th44: :: XXREAL_2:44
theorem :: XXREAL_2:45
theorem Th46: :: XXREAL_2:46
theorem :: XXREAL_2:47
theorem :: XXREAL_2:48
theorem Th49: :: XXREAL_2:49
theorem Th50: :: XXREAL_2:50
theorem Th52: :: XXREAL_2:51
theorem Th53: :: XXREAL_2:52
theorem :: XXREAL_2:53
theorem :: XXREAL_2:54
theorem :: XXREAL_2:55
theorem :: XXREAL_2:56
theorem Th57: :: XXREAL_2:57
theorem Th58: :: XXREAL_2:58
theorem Th59: :: XXREAL_2:59
theorem Th60: :: XXREAL_2:60
theorem :: XXREAL_2:61
theorem :: XXREAL_2:62
theorem :: XXREAL_2:63
theorem :: XXREAL_2:64
theorem Th69: :: XXREAL_2:65
theorem Th70: :: XXREAL_2:66
theorem :: XXREAL_2:67
theorem :: XXREAL_2:68
theorem Th69: :: XXREAL_2:69
theorem Th70: :: XXREAL_2:70
theorem :: XXREAL_2:71
theorem :: XXREAL_2:72
theorem Th73: :: XXREAL_2:73
theorem :: XXREAL_2:74
theorem Th75: :: XXREAL_2:75
theorem Th76: :: XXREAL_2:76
theorem :: XXREAL_2:77
theorem :: XXREAL_2:78
:: deftheorem Def12 defines connected XXREAL_2:def 12 :
theorem :: XXREAL_2:79
theorem :: XXREAL_2:80
theorem :: XXREAL_2:81
theorem Th82: :: XXREAL_2:82
theorem :: XXREAL_2:83
theorem Th84: :: XXREAL_2:84
theorem Th85: :: XXREAL_2:85
theorem Th86: :: XXREAL_2:86
theorem :: XXREAL_2:87
theorem Th88: :: XXREAL_2:88
theorem :: XXREAL_2:89
theorem :: XXREAL_2:90
theorem :: XXREAL_2:91
theorem Th89: :: XXREAL_2:92
theorem :: XXREAL_2:93
theorem :: XXREAL_2:94
theorem :: XXREAL_2:95