:: SUPINF_1 semantic presentation

definition

func +infty -> set equals :: SUPINF_1:def 1
REAL ;
correctness ;

end;

:: deftheorem Def1 defines +infty SUPINF_1:def 1 :

theorem Th1: :: SUPINF_1:1

canceled;

theorem Th2: :: SUPINF_1:2

not +infty in REAL ;

definition

let c₁ be set ;
attr a₁ is +Inf-like means :Def2: :: SUPINF_1:def 2
a₁ = +infty ;

end;

:: deftheorem Def2 defines +Inf-like SUPINF_1:def 2 :

registration

cluster +Inf-like set ;
existence

proof end;

end;

definition

mode +Inf is +Inf-like set ;

end;

theorem Th3: :: SUPINF_1:3

canceled;

theorem Th4: :: SUPINF_1:4

+infty is +Inf by Def2;

definition

func -infty -> set equals :: SUPINF_1:def 3
{REAL };
correctness ;

end;

:: deftheorem Def3 defines -infty SUPINF_1:def 3 :

theorem Th5: :: SUPINF_1:5

canceled;

theorem Th6: :: SUPINF_1:6

not -infty in REAL by TARSKI:def 1;

definition

let c₁ be set ;
attr a₁ is -Inf-like means :Def4: :: SUPINF_1:def 4
a₁ = -infty ;

end;

:: deftheorem Def4 defines -Inf-like SUPINF_1:def 4 :

registration

cluster -Inf-like set ;
existence

proof end;

end;

definition

mode -Inf is -Inf-like set ;

end;

theorem Th7: :: SUPINF_1:7

canceled;

theorem Th8: :: SUPINF_1:8

-infty is -Inf by Def4;

definition

let c₁ be set ;
attr a₁ is ext-real means :Def5: :: SUPINF_1:def 5
a₁ in REAL \/ {-infty ,+infty };

end;

:: deftheorem Def5 defines ext-real SUPINF_1:def 5 :

registration

cluster ext-real set ;
existence

proof end;

end;

definition

func ExtREAL -> set equals :: SUPINF_1:def 6
REAL \/ {-infty ,+infty };
correctness ;

end;

:: deftheorem Def6 defines ExtREAL SUPINF_1:def 6 :

registration

cluster -> ext-real Element of ExtREAL ;
coherence by Def5;

end;

definition

mode R_eal is Element of ExtREAL ;

end;

registration

cluster -> ext-real Element of REAL ;
coherence

proof end;

end;

theorem Th9: :: SUPINF_1:9

canceled;

theorem Th10: :: SUPINF_1:10

for b₁ being Real holds b₁ is R_eal by Def5;

theorem Th11: :: SUPINF_1:11

for b₁ being set st ( b₁ = -infty or b₁ = +infty ) holds
b₁ is R_eal

proof end;

definition

redefine func +infty as +infty -> R_eal;
coherence by Th11;
redefine func -infty as -infty -> R_eal;
coherence by Th11;

end;

theorem Th12: :: SUPINF_1:12

canceled;

theorem Th13: :: SUPINF_1:13

canceled;

theorem Th14: :: SUPINF_1:14

-infty <> +infty

proof end;

Lemma8: for b₁ being R_eal holds
( b₁ in REAL or b₁ = +infty or b₁ = -infty )

proof end;

definition

let c₁, c₂ be R_eal;
pred c₁ <=' c₂ means :Def7: :: SUPINF_1:def 7
ex b₁, b₂ being Real st
( b₁ = a₁ & b₂ = a₂ & b₁ <= b₂ ) if ( a₁ in REAL & a₂ in REAL )
otherwise ( a₁ = -infty or a₂ = +infty );
consistency ;
reflexivity by Lemma8;
connectedness

proof end;

end;

:: deftheorem Def7 defines <=' SUPINF_1:def 7 :

notation

let c₁, c₂ be R_eal;
antonym c₂ <' c₁ for c₁ <=' c₂;

end;

theorem Th15: :: SUPINF_1:15

canceled;

theorem Th16: :: SUPINF_1:16

for b₁, b₂ being R_eal st b₁ is Real & b₂ is Real holds
( b₁ <=' b₂ iff ex b₃, b₄ being Real st
( b₃ = b₁ & b₄ = b₂ & b₃ <= b₄ ) ) by Def7;

theorem Th17: :: SUPINF_1:17

for b₁ being R_eal st b₁ in REAL holds
not b₁ <=' -infty by Def7, Th6, Th14;

theorem Th18: :: SUPINF_1:18

for b₁ being R_eal st b₁ in REAL holds
not +infty <=' b₁ by Def7, Th2, Th14;

theorem Th19: :: SUPINF_1:19

not +infty <=' -infty by Def7, Th2, Th14;

theorem Th20: :: SUPINF_1:20

for b₁ being R_eal holds b₁ <=' +infty by Def7, Th2;

theorem Th21: :: SUPINF_1:21

for b₁ being R_eal holds -infty <=' b₁ by Def7, Th6;

theorem Th22: :: SUPINF_1:22

for b₁, b₂ being R_eal st b₁ <=' b₂ & b₂ <=' b₁ holds
b₁ = b₂

proof end;

theorem Th23: :: SUPINF_1:23

for b₁ being R_eal st b₁ <=' -infty holds
b₁ = -infty

proof end;

theorem Th24: :: SUPINF_1:24

for b₁ being R_eal st +infty <=' b₁ holds
b₁ = +infty

proof end;

scheme :: SUPINF_1:sch 1
s1{ P₁[ R_eal] } :

ex b₁ being Subset of (REAL \/ {-infty ,+infty }) st
for b₂ being R_eal holds
( b₂ in b₁ iff P₁[b₂] )

proof end;

theorem Th25: :: SUPINF_1:25

canceled;

theorem Th26: :: SUPINF_1:26

ExtREAL is non empty set ;

theorem Th27: :: SUPINF_1:27

for b₁ being set holds
( b₁ is R_eal iff b₁ in ExtREAL ) ;

theorem Th28: :: SUPINF_1:28

canceled;

theorem Th29: :: SUPINF_1:29

for b₁, b₂, b₃ being R_eal st b₁ <=' b₂ & b₂ <=' b₃ holds
b₁ <=' b₃

proof end;

registration

cluster ExtREAL -> non empty ;
coherence ;

end;

theorem Th30: :: SUPINF_1:30

canceled;

theorem Th31: :: SUPINF_1:31

for b₁ being R_eal st b₁ in REAL holds
( -infty <' b₁ & b₁ <' +infty )

proof end;

definition

let c₁ be Subset of ExtREAL ;
canceled;
mode majorant of c₁ -> R_eal means :Def9: :: SUPINF_1:def 9
for b₁ being R_eal st b₁ in a₁ holds
b₁ <=' a₂;
existence

proof end;

end;

:: deftheorem Def8 SUPINF_1:def 8 :

:: deftheorem Def9 defines majorant SUPINF_1:def 9 :

theorem Th32: :: SUPINF_1:32

canceled;

theorem Th33: :: SUPINF_1:33

for b₁ being Subset of ExtREAL holds +infty is majorant of b₁

proof end;

theorem Th34: :: SUPINF_1:34

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ holds
for b₃ being R_eal st b₃ is majorant of b₂ holds
b₃ is majorant of b₁

proof end;

definition

let c₁ be Subset of ExtREAL ;
mode minorant of c₁ -> R_eal means :Def10: :: SUPINF_1:def 10
for b₁ being R_eal st b₁ in a₁ holds
a₂ <=' b₁;
existence

proof end;

end;

:: deftheorem Def10 defines minorant SUPINF_1:def 10 :

theorem Th35: :: SUPINF_1:35

canceled;

theorem Th36: :: SUPINF_1:36

for b₁ being Subset of ExtREAL holds -infty is minorant of b₁

proof end;

theorem Th37: :: SUPINF_1:37

canceled;

theorem Th38: :: SUPINF_1:38

canceled;

theorem Th39: :: SUPINF_1:39

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ holds
for b₃ being R_eal st b₃ is minorant of b₂ holds
b₃ is minorant of b₁

proof end;

definition

redefine func REAL as REAL -> non empty Subset of ExtREAL ;
coherence by XBOOLE_1:7;

end;

theorem Th40: :: SUPINF_1:40

canceled;

theorem Th41: :: SUPINF_1:41

+infty is majorant of REAL by Th33;

theorem Th42: :: SUPINF_1:42

-infty is minorant of REAL by Th36;

definition

let c₁ be Subset of ExtREAL ;
attr a₁ is bounded_above means :Def11: :: SUPINF_1:def 11
ex b₁ being majorant of a₁ st b₁ in REAL ;

end;

:: deftheorem Def11 defines bounded_above SUPINF_1:def 11 :

theorem Th43: :: SUPINF_1:43

canceled;

theorem Th44: :: SUPINF_1:44

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ & b₂ is bounded_above holds
b₁ is bounded_above

proof end;

theorem Th45: :: SUPINF_1:45

not REAL is bounded_above

proof end;

definition

let c₁ be Subset of ExtREAL ;
attr a₁ is bounded_below means :Def12: :: SUPINF_1:def 12
ex b₁ being minorant of a₁ st b₁ in REAL ;

end;

:: deftheorem Def12 defines bounded_below SUPINF_1:def 12 :

theorem Th46: :: SUPINF_1:46

canceled;

theorem Th47: :: SUPINF_1:47

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ & b₂ is bounded_below holds
b₁ is bounded_below

proof end;

theorem Th48: :: SUPINF_1:48

not REAL is bounded_below

proof end;

definition

let c₁ be Subset of ExtREAL ;
attr a₁ is bounded means :Def13: :: SUPINF_1:def 13
( a₁ is bounded_above & a₁ is bounded_below );

end;

:: deftheorem Def13 defines bounded SUPINF_1:def 13 :

theorem Th49: :: SUPINF_1:49

canceled;

theorem Th50: :: SUPINF_1:50

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ & b₂ is bounded holds
b₁ is bounded

proof end;

theorem Th51: :: SUPINF_1:51

for b₁ being Subset of ExtREAL ex b₂ being non empty Subset of ExtREAL st
for b₃ being R_eal holds
( b₃ in b₂ iff b₃ is majorant of b₁ )

proof end;

definition

let c₁ be Subset of ExtREAL ;
func SetMajorant c₁ -> Subset of ExtREAL means :Def14: :: SUPINF_1:def 14
for b₁ being R_eal holds
( b₁ in a₂ iff b₁ is majorant of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines SetMajorant SUPINF_1:def 14 :

registration

let c₁ be Subset of ExtREAL ;
cluster SetMajorant a₁ -> non empty ;
coherence

proof end;

end;

theorem Th52: :: SUPINF_1:52

canceled;

theorem Th53: :: SUPINF_1:53

canceled;

theorem Th54: :: SUPINF_1:54

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ holds
for b₃ being R_eal st b₃ in SetMajorant b₂ holds
b₃ in SetMajorant b₁

proof end;

theorem Th55: :: SUPINF_1:55

for b₁ being Subset of ExtREAL ex b₂ being non empty Subset of ExtREAL st
for b₃ being R_eal holds
( b₃ in b₂ iff b₃ is minorant of b₁ )

proof end;

definition

let c₁ be Subset of ExtREAL ;
func SetMinorant c₁ -> Subset of ExtREAL means :Def15: :: SUPINF_1:def 15
for b₁ being R_eal holds
( b₁ in a₂ iff b₁ is minorant of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines SetMinorant SUPINF_1:def 15 :

registration

let c₁ be Subset of ExtREAL ;
cluster SetMinorant a₁ -> non empty ;
coherence

proof end;

end;

theorem Th56: :: SUPINF_1:56

canceled;

theorem Th57: :: SUPINF_1:57

canceled;

theorem Th58: :: SUPINF_1:58

for b₁, b₂ being Subset of ExtREAL st b₁ c= b₂ holds
for b₃ being R_eal st b₃ in SetMinorant b₂ holds
b₃ in SetMinorant b₁

proof end;

theorem Th59: :: SUPINF_1:59

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_above & not b₁ = {-infty } holds
ex b₂ being Real st
( b₂ in b₁ & not b₂ = -infty )

proof end;

theorem Th60: :: SUPINF_1:60

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_below & not b₁ = {+infty } holds
ex b₂ being Real st
( b₂ in b₁ & not b₂ = +infty )

proof end;

theorem Th61: :: SUPINF_1:61

canceled;

theorem Th62: :: SUPINF_1:62

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_above & not b₁ = {-infty } holds
ex b₂ being R_eal st
( b₂ is majorant of b₁ & ( for b₃ being R_eal st b₃ is majorant of b₁ holds
b₂ <=' b₃ ) )

proof end;

theorem Th63: :: SUPINF_1:63

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_below & not b₁ = {+infty } holds
ex b₂ being R_eal st
( b₂ is minorant of b₁ & ( for b₃ being R_eal st b₃ is minorant of b₁ holds
b₃ <=' b₂ ) )

proof end;

theorem Th64: :: SUPINF_1:64

for b₁ being Subset of ExtREAL st b₁ = {-infty } holds
b₁ is bounded_above

proof end;

theorem Th65: :: SUPINF_1:65

for b₁ being Subset of ExtREAL st b₁ = {+infty } holds
b₁ is bounded_below

proof end;

theorem Th66: :: SUPINF_1:66

for b₁ being Subset of ExtREAL st b₁ = {-infty } holds
ex b₂ being R_eal st
( b₂ is majorant of b₁ & ( for b₃ being R_eal st b₃ is majorant of b₁ holds
b₂ <=' b₃ ) )

proof end;

theorem Th67: :: SUPINF_1:67

for b₁ being Subset of ExtREAL st b₁ = {+infty } holds
ex b₂ being R_eal st
( b₂ is minorant of b₁ & ( for b₃ being R_eal st b₃ is minorant of b₁ holds
b₃ <=' b₂ ) )

proof end;

theorem Th68: :: SUPINF_1:68

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_above holds
ex b₂ being R_eal st
( b₂ is majorant of b₁ & ( for b₃ being R_eal st b₃ is majorant of b₁ holds
b₂ <=' b₃ ) )

proof end;

theorem Th69: :: SUPINF_1:69

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_below holds
ex b₂ being R_eal st
( b₂ is minorant of b₁ & ( for b₃ being R_eal st b₃ is minorant of b₁ holds
b₃ <=' b₂ ) )

proof end;

theorem Th70: :: SUPINF_1:70

for b₁ being non empty Subset of ExtREAL st not b₁ is bounded_above holds
for b₂ being R_eal st b₂ is majorant of b₁ holds
b₂ = +infty

proof end;

theorem Th71: :: SUPINF_1:71

for b₁ being non empty Subset of ExtREAL st not b₁ is bounded_below holds
for b₂ being R_eal st b₂ is minorant of b₁ holds
b₂ = -infty

proof end;

theorem Th72: :: SUPINF_1:72

for b₁ being non empty Subset of ExtREAL ex b₂ being R_eal st
( b₂ is majorant of b₁ & ( for b₃ being R_eal st b₃ is majorant of b₁ holds
b₂ <=' b₃ ) )

proof end;

theorem Th73: :: SUPINF_1:73

for b₁ being non empty Subset of ExtREAL ex b₂ being R_eal st
( b₂ is minorant of b₁ & ( for b₃ being R_eal st b₃ is minorant of b₁ holds
b₃ <=' b₂ ) )

proof end;

definition

let c₁ be non empty Subset of ExtREAL ;
func sup c₁ -> R_eal means :Def16: :: SUPINF_1:def 16
( a₂ is majorant of a₁ & ( for b₁ being R_eal st b₁ is majorant of a₁ holds
a₂ <=' b₁ ) );
existence by Th72;
uniqueness

proof end;

end;

:: deftheorem Def16 defines sup SUPINF_1:def 16 :

theorem Th74: :: SUPINF_1:74

canceled;

theorem Th75: :: SUPINF_1:75

canceled;

theorem Th76: :: SUPINF_1:76

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal st b₂ in b₁ holds
b₂ <=' sup b₁

proof end;

definition

let c₁ be non empty Subset of ExtREAL ;
func inf c₁ -> R_eal means :Def17: :: SUPINF_1:def 17
( a₂ is minorant of a₁ & ( for b₁ being R_eal st b₁ is minorant of a₁ holds
b₁ <=' a₂ ) );
existence by Th73;
uniqueness

proof end;

end;

:: deftheorem Def17 defines inf SUPINF_1:def 17 :

theorem Th77: :: SUPINF_1:77

canceled;

theorem Th78: :: SUPINF_1:78

canceled;

theorem Th79: :: SUPINF_1:79

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal st b₂ in b₁ holds
inf b₁ <=' b₂

proof end;

theorem Th80: :: SUPINF_1:80

for b₁ being non empty Subset of ExtREAL
for b₂ being majorant of b₁ st b₂ in b₁ holds
b₂ = sup b₁

proof end;

theorem Th81: :: SUPINF_1:81

for b₁ being non empty Subset of ExtREAL
for b₂ being minorant of b₁ st b₂ in b₁ holds
b₂ = inf b₁

proof end;

theorem Th82: :: SUPINF_1:82

for b₁ being non empty Subset of ExtREAL holds
( sup b₁ = inf (SetMajorant b₁) & inf b₁ = sup (SetMinorant b₁) )

proof end;

theorem Th83: :: SUPINF_1:83

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_above & not b₁ = {-infty } holds
sup b₁ in REAL

proof end;

theorem Th84: :: SUPINF_1:84

for b₁ being non empty Subset of ExtREAL st b₁ is bounded_below & not b₁ = {+infty } holds
inf b₁ in REAL

proof end;

definition

let c₁ be R_eal;
redefine func { as {c₁} -> Subset of ExtREAL ;
coherence by ZFMISC_1:37;

end;

definition

let c₁, c₂ be R_eal;
redefine func { as {c₁,c₂} -> Subset of ExtREAL ;
coherence by ZFMISC_1:38;

end;

theorem Th85: :: SUPINF_1:85

for b₁ being R_eal holds sup {b₁} = b₁

proof end;

theorem Th86: :: SUPINF_1:86

for b₁ being R_eal holds inf {b₁} = b₁

proof end;

theorem Th87: :: SUPINF_1:87

canceled;

theorem Th88: :: SUPINF_1:88

canceled;

theorem Th89: :: SUPINF_1:89

canceled;

theorem Th90: :: SUPINF_1:90

canceled;

theorem Th91: :: SUPINF_1:91

for b₁, b₂ being non empty Subset of ExtREAL st b₁ c= b₂ holds
sup b₁ <=' sup b₂

proof end;

theorem Th92: :: SUPINF_1:92

for b₁, b₂, b₃ being R_eal st b₁ <=' b₃ & b₂ <=' b₃ holds
sup {b₁,b₂} <=' b₃

proof end;

theorem Th93: :: SUPINF_1:93

for b₁, b₂ being R_eal holds
( ( b₁ <=' b₂ implies sup {b₁,b₂} = b₂ ) & ( b₂ <=' b₁ implies sup {b₁,b₂} = b₁ ) )

proof end;

theorem Th94: :: SUPINF_1:94

for b₁, b₂ being non empty Subset of ExtREAL st b₁ c= b₂ holds
inf b₂ <=' inf b₁

proof end;

theorem Th95: :: SUPINF_1:95

for b₁, b₂, b₃ being R_eal st b₃ <=' b₁ & b₃ <=' b₂ holds
b₃ <=' inf {b₁,b₂}

proof end;

theorem Th96: :: SUPINF_1:96

for b₁, b₂ being R_eal holds
( ( b₁ <=' b₂ implies inf {b₁,b₂} = b₁ ) & ( b₂ <=' b₁ implies inf {b₁,b₂} = b₂ ) )

proof end;

theorem Th97: :: SUPINF_1:97

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal st ex b₃ being R_eal st
( b₃ in b₁ & b₂ <=' b₃ ) holds
b₂ <=' sup b₁

proof end;

theorem Th98: :: SUPINF_1:98

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal st ex b₃ being R_eal st
( b₃ in b₁ & b₃ <=' b₂ ) holds
inf b₁ <=' b₂

proof end;

theorem Th99: :: SUPINF_1:99

for b₁, b₂ being non empty Subset of ExtREAL st ( for b₃ being R_eal st b₃ in b₁ holds
ex b₄ being R_eal st
( b₄ in b₂ & b₃ <=' b₄ ) ) holds
sup b₁ <=' sup b₂

proof end;

theorem Th100: :: SUPINF_1:100

for b₁, b₂ being non empty Subset of ExtREAL st ( for b₃ being R_eal st b₃ in b₂ holds
ex b₄ being R_eal st
( b₄ in b₁ & b₄ <=' b₃ ) ) holds
inf b₁ <=' inf b₂

proof end;

theorem Th101: :: SUPINF_1:101

for b₁, b₂ being Subset of ExtREAL
for b₃ being majorant of b₁
for b₄ being majorant of b₂ holds sup {b₃,b₄} is majorant of b₁ \/ b₂

proof end;

theorem Th102: :: SUPINF_1:102

for b₁, b₂ being Subset of ExtREAL
for b₃ being minorant of b₁
for b₄ being minorant of b₂ holds inf {b₃,b₄} is minorant of b₁ \/ b₂

proof end;

theorem Th103: :: SUPINF_1:103

for b₁, b₂, b₃ being Subset of ExtREAL
for b₄ being majorant of b₁
for b₅ being majorant of b₂ st b₃ = b₁ /\ b₂ holds
inf {b₄,b₅} is majorant of b₃

proof end;

theorem Th104: :: SUPINF_1:104

for b₁, b₂, b₃ being Subset of ExtREAL
for b₄ being minorant of b₁
for b₅ being minorant of b₂ st b₃ = b₁ /\ b₂ holds
sup {b₄,b₅} is minorant of b₃

proof end;

theorem Th105: :: SUPINF_1:105

for b₁, b₂ being non empty Subset of ExtREAL holds sup (b₁ \/ b₂) = sup {(sup b₁),(sup b₂)}

proof end;

theorem Th106: :: SUPINF_1:106

for b₁, b₂ being non empty Subset of ExtREAL holds inf (b₁ \/ b₂) = inf {(inf b₁),(inf b₂)}

proof end;

theorem Th107: :: SUPINF_1:107

for b₁, b₂, b₃ being non empty Subset of ExtREAL st b₃ = b₁ /\ b₂ holds
sup b₃ <=' inf {(sup b₁),(sup b₂)}

proof end;

theorem Th108: :: SUPINF_1:108

for b₁, b₂, b₃ being non empty Subset of ExtREAL st b₃ = b₁ /\ b₂ holds
sup {(inf b₁),(inf b₂)} <=' inf b₃

proof end;

definition

let c₁ be non empty set ;
mode bool_DOMAIN of c₁ -> set means :Def18: :: SUPINF_1:def 18
( a₂ is non empty Subset-Family of a₁ & ( for b₁ being set st b₁ in a₂ holds
b₁ is non empty set ) );
existence

proof end;

end;

:: deftheorem Def18 defines bool_DOMAIN SUPINF_1:def 18 :

definition

let c₁ be bool_DOMAIN of ExtREAL ;
func SUP c₁ -> Subset of ExtREAL means :Def19: :: SUPINF_1:def 19
for b₁ being R_eal holds
( b₁ in a₂ iff ex b₂ being non empty Subset of ExtREAL st
( b₂ in a₁ & b₁ = sup b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines SUP SUPINF_1:def 19 :

registration

let c₁ be bool_DOMAIN of ExtREAL ;
cluster SUP a₁ -> non empty ;
coherence

proof end;

end;

theorem Th109: :: SUPINF_1:109

canceled;

theorem Th110: :: SUPINF_1:110

canceled;

theorem Th111: :: SUPINF_1:111

canceled;

theorem Th112: :: SUPINF_1:112

for b₁ being bool_DOMAIN of ExtREAL
for b₂ being non empty Subset of ExtREAL st b₂ = union b₁ holds
sup b₂ is majorant of SUP b₁

proof end;

theorem Th113: :: SUPINF_1:113

for b₁ being bool_DOMAIN of ExtREAL
for b₂ being Subset of ExtREAL st b₂ = union b₁ holds
sup (SUP b₁) is majorant of b₂

proof end;

theorem Th114: :: SUPINF_1:114

for b₁ being bool_DOMAIN of ExtREAL
for b₂ being non empty Subset of ExtREAL st b₂ = union b₁ holds
sup b₂ = sup (SUP b₁)

proof end;

definition

let c₁ be bool_DOMAIN of ExtREAL ;
func INF c₁ -> Subset of ExtREAL means :Def20: :: SUPINF_1:def 20
for b₁ being R_eal holds
( b₁ in a₂ iff ex b₂ being non empty Subset of ExtREAL st
( b₂ in a₁ & b₁ = inf b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines INF SUPINF_1:def 20 :

registration

let c₁ be bool_DOMAIN of ExtREAL ;
cluster INF a₁ -> non empty ;
coherence

proof end;

end;

theorem Th115: :: SUPINF_1:115

canceled;

theorem Th116: :: SUPINF_1:116

canceled;

theorem Th117: :: SUPINF_1:117

for b₁ being bool_DOMAIN of ExtREAL
for b₂ being non empty Subset of ExtREAL st b₂ = union b₁ holds
inf b₂ is minorant of INF b₁

proof end;

theorem Th118: :: SUPINF_1:118

for b₁ being bool_DOMAIN of ExtREAL
for b₂ being Subset of ExtREAL st b₂ = union b₁ holds
inf (INF b₁) is minorant of b₂

proof end;

theorem Th119: :: SUPINF_1:119

for b₁ being bool_DOMAIN of ExtREAL
for b₂ being non empty Subset of ExtREAL st b₂ = union b₁ holds
inf b₂ = inf (INF b₁)

proof end;

theorem Th120: :: SUPINF_1:120

for b₁, b₂ being R_eal
for b₃, b₄ being real number st b₁ = b₃ & b₂ = b₄ holds
( b₃ <= b₄ iff b₁ <=' b₂ )

proof end;