:: SUPINF_1 semantic presentation

definition

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

end;

:: deftheorem defines +infty SUPINF_1:def 1 :

theorem :: SUPINF_1:1

canceled;

theorem Th2: :: SUPINF_1:2

not +infty in REAL ;

definition

let IT be set ;
attr IT is +Inf-like means :Def2: :: SUPINF_1:def 2
IT = +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 :: SUPINF_1:3

canceled;

theorem :: SUPINF_1:4

+infty is +Inf by Def2;

definition

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

end;

:: deftheorem defines -infty SUPINF_1:def 3 :

theorem :: SUPINF_1:5

canceled;

theorem Th6: :: SUPINF_1:6

not -infty in REAL by TARSKI:def 1;

definition

let IT be set ;
attr IT is -Inf-like means :Def4: :: SUPINF_1:def 4
IT = -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 :: SUPINF_1:7

canceled;

theorem :: SUPINF_1:8

-infty is -Inf by Def4;

definition

let IT be set ;
attr IT is ext-real means :Def5: :: SUPINF_1:def 5
IT 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 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 :: SUPINF_1:9

canceled;

theorem :: SUPINF_1:10

for x being Real holds x is R_eal by Def5;

theorem Th11: :: SUPINF_1:11

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

proof end;

definition

:: original: +infty
redefine func +infty -> R_eal;
coherence by Th11;
:: original: -infty
redefine func -infty -> R_eal;
coherence by Th11;

end;

theorem :: SUPINF_1:12

canceled;

theorem :: SUPINF_1:13

canceled;

theorem Th14: :: SUPINF_1:14

-infty <> +infty

proof end;

Lm1: for x being R_eal holds
( x in REAL or x = +infty or x = -infty )

proof end;

definition

let x, y be R_eal;
pred x <=' y means :Def7: :: SUPINF_1:def 7
ex p, q being Real st
( p = x & q = y & p <= q ) if ( x in REAL & y in REAL )
otherwise ( x = -infty or y = +infty );
consistency ;
reflexivity by Lm1;
connectedness

proof end;

end;

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

notation

let x, y be R_eal;
antonym y <' x for x <=' y;

end;

theorem :: SUPINF_1:15

canceled;

theorem :: SUPINF_1:16

for x, y being R_eal st x is Real & y is Real holds
( x <=' y iff ex p, q being Real st
( p = x & q = y & p <= q ) ) by Def7;

theorem Th17: :: SUPINF_1:17

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

theorem Th18: :: SUPINF_1:18

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

theorem :: SUPINF_1:19

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

theorem :: SUPINF_1:20

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

theorem :: SUPINF_1:21

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

theorem Th22: :: SUPINF_1:22

for x, y being R_eal st x <=' y & y <=' x holds
x = y

proof end;

theorem :: SUPINF_1:23

for x being R_eal st x <=' -infty holds
x = -infty

proof end;

theorem Th24: :: SUPINF_1:24

for x being R_eal st +infty <=' x holds
x = +infty

proof end;

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

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

proof end;

theorem :: SUPINF_1:25

canceled;

theorem :: SUPINF_1:26

ExtREAL is non empty set ;

theorem :: SUPINF_1:27

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

theorem :: SUPINF_1:28

canceled;

theorem Th29: :: SUPINF_1:29

for x, y, z being R_eal st x <=' y & y <=' z holds
x <=' z

proof end;

registration

cluster ExtREAL -> non empty ;
coherence ;

end;

theorem :: SUPINF_1:30

canceled;

theorem :: SUPINF_1:31

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

proof end;

definition

let X be Subset of ExtREAL ;
canceled;
mode majorant of X -> R_eal means :Def9: :: SUPINF_1:def 9
for x being R_eal st x in X holds
x <=' it;
existence

proof end;

end;

:: deftheorem SUPINF_1:def 8 :

:: deftheorem Def9 defines majorant SUPINF_1:def 9 :

theorem :: SUPINF_1:32

canceled;

theorem Th33: :: SUPINF_1:33

for X being Subset of ExtREAL holds +infty is majorant of X

proof end;

theorem Th34: :: SUPINF_1:34

for X, Y being Subset of ExtREAL st X c= Y holds
for UB being R_eal st UB is majorant of Y holds
UB is majorant of X

proof end;

definition

let X be Subset of ExtREAL ;
mode minorant of X -> R_eal means :Def10: :: SUPINF_1:def 10
for x being R_eal st x in X holds
it <=' x;
existence

proof end;

end;

:: deftheorem Def10 defines minorant SUPINF_1:def 10 :

theorem :: SUPINF_1:35

canceled;

theorem Th36: :: SUPINF_1:36

for X being Subset of ExtREAL holds -infty is minorant of X

proof end;

theorem :: SUPINF_1:37

canceled;

theorem :: SUPINF_1:38

canceled;

theorem Th39: :: SUPINF_1:39

for X, Y being Subset of ExtREAL st X c= Y holds
for LB being R_eal st LB is minorant of Y holds
LB is minorant of X

proof end;

definition

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

end;

theorem :: SUPINF_1:40

canceled;

theorem :: SUPINF_1:41

+infty is majorant of REAL by Th33;

theorem :: SUPINF_1:42

-infty is minorant of REAL by Th36;

definition

let X be Subset of ExtREAL ;
attr X is bounded_above means :Def11: :: SUPINF_1:def 11
ex UB being majorant of X st UB in REAL ;

end;

:: deftheorem Def11 defines bounded_above SUPINF_1:def 11 :

theorem :: SUPINF_1:43

canceled;

theorem Th44: :: SUPINF_1:44

for X, Y being Subset of ExtREAL st X c= Y & Y is bounded_above holds
X is bounded_above

proof end;

theorem :: SUPINF_1:45

not REAL is bounded_above

proof end;

definition

let X be Subset of ExtREAL ;
attr X is bounded_below means :Def12: :: SUPINF_1:def 12
ex LB being minorant of X st LB in REAL ;

end;

:: deftheorem Def12 defines bounded_below SUPINF_1:def 12 :

theorem :: SUPINF_1:46

canceled;

theorem Th47: :: SUPINF_1:47

for X, Y being Subset of ExtREAL st X c= Y & Y is bounded_below holds
X is bounded_below

proof end;

theorem :: SUPINF_1:48

not REAL is bounded_below

proof end;

definition

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

end;

:: deftheorem Def13 defines bounded SUPINF_1:def 13 :

theorem :: SUPINF_1:49

canceled;

theorem :: SUPINF_1:50

for X, Y being Subset of ExtREAL st X c= Y & Y is bounded holds
X is bounded

proof end;

theorem Th51: :: SUPINF_1:51

for X being Subset of ExtREAL ex Y being non empty Subset of ExtREAL st
for x being R_eal holds
( x in Y iff x is majorant of X )

proof end;

definition

let X be Subset of ExtREAL ;
func SetMajorant X -> Subset of ExtREAL means :Def14: :: SUPINF_1:def 14
for x being R_eal holds
( x in it iff x is majorant of X );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines SetMajorant SUPINF_1:def 14 :

registration

let X be Subset of ExtREAL ;
cluster SetMajorant X -> non empty ;
coherence

proof end;

end;

theorem :: SUPINF_1:52

canceled;

theorem :: SUPINF_1:53

canceled;

theorem :: SUPINF_1:54

for X, Y being Subset of ExtREAL st X c= Y holds
for x being R_eal st x in SetMajorant Y holds
x in SetMajorant X

proof end;

theorem Th55: :: SUPINF_1:55

for X being Subset of ExtREAL ex Y being non empty Subset of ExtREAL st
for x being R_eal holds
( x in Y iff x is minorant of X )

proof end;

definition

let X be Subset of ExtREAL ;
func SetMinorant X -> Subset of ExtREAL means :Def15: :: SUPINF_1:def 15
for x being R_eal holds
( x in it iff x is minorant of X );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines SetMinorant SUPINF_1:def 15 :

registration

let X be Subset of ExtREAL ;
cluster SetMinorant X -> non empty ;
coherence

proof end;

end;

theorem :: SUPINF_1:56

canceled;

theorem :: SUPINF_1:57

canceled;

theorem :: SUPINF_1:58

for X, Y being Subset of ExtREAL st X c= Y holds
for x being R_eal st x in SetMinorant Y holds
x in SetMinorant X

proof end;

theorem Th59: :: SUPINF_1:59

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

proof end;

theorem Th60: :: SUPINF_1:60

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

proof end;

theorem :: SUPINF_1:61

canceled;

theorem Th62: :: SUPINF_1:62

for X being non empty Subset of ExtREAL st X is bounded_above & not X = {-infty } holds
ex UB being R_eal st
( UB is majorant of X & ( for y being R_eal st y is majorant of X holds
UB <=' y ) )

proof end;

theorem Th63: :: SUPINF_1:63

for X being non empty Subset of ExtREAL st X is bounded_below & not X = {+infty } holds
ex LB being R_eal st
( LB is minorant of X & ( for y being R_eal st y is minorant of X holds
y <=' LB ) )

proof end;

theorem Th64: :: SUPINF_1:64

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

proof end;

theorem Th65: :: SUPINF_1:65

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

proof end;

theorem Th66: :: SUPINF_1:66

for X being Subset of ExtREAL st X = {-infty } holds
ex UB being R_eal st
( UB is majorant of X & ( for y being R_eal st y is majorant of X holds
UB <=' y ) )

proof end;

theorem Th67: :: SUPINF_1:67

for X being Subset of ExtREAL st X = {+infty } holds
ex LB being R_eal st
( LB is minorant of X & ( for y being R_eal st y is minorant of X holds
y <=' LB ) )

proof end;

theorem Th68: :: SUPINF_1:68

for X being non empty Subset of ExtREAL st X is bounded_above holds
ex UB being R_eal st
( UB is majorant of X & ( for y being R_eal st y is majorant of X holds
UB <=' y ) )

proof end;

theorem Th69: :: SUPINF_1:69

for X being non empty Subset of ExtREAL st X is bounded_below holds
ex LB being R_eal st
( LB is minorant of X & ( for y being R_eal st y is minorant of X holds
y <=' LB ) )

proof end;

theorem Th70: :: SUPINF_1:70

for X being non empty Subset of ExtREAL st not X is bounded_above holds
for y being R_eal st y is majorant of X holds
y = +infty

proof end;

theorem Th71: :: SUPINF_1:71

for X being non empty Subset of ExtREAL st not X is bounded_below holds
for y being R_eal st y is minorant of X holds
y = -infty

proof end;

theorem Th72: :: SUPINF_1:72

for X being non empty Subset of ExtREAL ex UB being R_eal st
( UB is majorant of X & ( for y being R_eal st y is majorant of X holds
UB <=' y ) )

proof end;

theorem Th73: :: SUPINF_1:73

for X being non empty Subset of ExtREAL ex LB being R_eal st
( LB is minorant of X & ( for y being R_eal st y is minorant of X holds
y <=' LB ) )

proof end;

definition

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

proof end;

end;

:: deftheorem Def16 defines sup SUPINF_1:def 16 :

theorem :: SUPINF_1:74

canceled;

theorem :: SUPINF_1:75

canceled;

theorem Th76: :: SUPINF_1:76

for X being non empty Subset of ExtREAL
for x being R_eal st x in X holds
x <=' sup X

proof end;

definition

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

proof end;

end;

:: deftheorem Def17 defines inf SUPINF_1:def 17 :

theorem :: SUPINF_1:77

canceled;

theorem :: SUPINF_1:78

canceled;

theorem Th79: :: SUPINF_1:79

for X being non empty Subset of ExtREAL
for x being R_eal st x in X holds
inf X <=' x

proof end;

theorem Th80: :: SUPINF_1:80

for X being non empty Subset of ExtREAL
for x being majorant of X st x in X holds
x = sup X

proof end;

theorem Th81: :: SUPINF_1:81

for X being non empty Subset of ExtREAL
for x being minorant of X st x in X holds
x = inf X

proof end;

theorem :: SUPINF_1:82

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

proof end;

theorem :: SUPINF_1:83

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

proof end;

theorem :: SUPINF_1:84

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

proof end;

definition

let x be R_eal;
:: original: {
redefine func {x} -> Subset of ExtREAL ;
coherence by ZFMISC_1:37;

end;

definition

let x, y be R_eal;
:: original: {
redefine func {x,y} -> Subset of ExtREAL ;
coherence by ZFMISC_1:38;

end;

theorem :: SUPINF_1:85

for x being R_eal holds sup {x} = x

proof end;

theorem :: SUPINF_1:86

for x being R_eal holds inf {x} = x

proof end;

theorem :: SUPINF_1:87

canceled;

theorem :: SUPINF_1:88

canceled;

theorem :: SUPINF_1:89

canceled;

theorem :: SUPINF_1:90

canceled;

theorem Th91: :: SUPINF_1:91

for X, Y being non empty Subset of ExtREAL st X c= Y holds
sup X <=' sup Y

proof end;

theorem Th92: :: SUPINF_1:92

for x, y, a being R_eal st x <=' a & y <=' a holds
sup {x,y} <=' a

proof end;

theorem :: SUPINF_1:93

for x, y being R_eal holds
( ( x <=' y implies sup {x,y} = y ) & ( y <=' x implies sup {x,y} = x ) )

proof end;

theorem Th94: :: SUPINF_1:94

for X, Y being non empty Subset of ExtREAL st X c= Y holds
inf Y <=' inf X

proof end;

theorem Th95: :: SUPINF_1:95

for x, y, a being R_eal st a <=' x & a <=' y holds
a <=' inf {x,y}

proof end;

theorem :: SUPINF_1:96

for x, y being R_eal holds
( ( x <=' y implies inf {x,y} = x ) & ( y <=' x implies inf {x,y} = y ) )

proof end;

theorem Th97: :: SUPINF_1:97

for X being non empty Subset of ExtREAL
for x being R_eal st ex y being R_eal st
( y in X & x <=' y ) holds
x <=' sup X

proof end;

theorem Th98: :: SUPINF_1:98

for X being non empty Subset of ExtREAL
for x being R_eal st ex y being R_eal st
( y in X & y <=' x ) holds
inf X <=' x

proof end;

theorem :: SUPINF_1:99

for X, Y being non empty Subset of ExtREAL st ( for x being R_eal st x in X holds
ex y being R_eal st
( y in Y & x <=' y ) ) holds
sup X <=' sup Y

proof end;

theorem :: SUPINF_1:100

for X, Y being non empty Subset of ExtREAL st ( for y being R_eal st y in Y holds
ex x being R_eal st
( x in X & x <=' y ) ) holds
inf X <=' inf Y

proof end;

theorem Th101: :: SUPINF_1:101

for X, Y being Subset of ExtREAL
for UB1 being majorant of X
for UB2 being majorant of Y holds sup {UB1,UB2} is majorant of X \/ Y

proof end;

theorem Th102: :: SUPINF_1:102

for X, Y being Subset of ExtREAL
for LB1 being minorant of X
for LB2 being minorant of Y holds inf {LB1,LB2} is minorant of X \/ Y

proof end;

theorem Th103: :: SUPINF_1:103

for X, Y, S being Subset of ExtREAL
for UB1 being majorant of X
for UB2 being majorant of Y st S = X /\ Y holds
inf {UB1,UB2} is majorant of S

proof end;

theorem Th104: :: SUPINF_1:104

for X, Y, S being Subset of ExtREAL
for LB1 being minorant of X
for LB2 being minorant of Y st S = X /\ Y holds
sup {LB1,LB2} is minorant of S

proof end;

theorem :: SUPINF_1:105

for X, Y being non empty Subset of ExtREAL holds sup (X \/ Y) = sup {(sup X),(sup Y)}

proof end;

theorem :: SUPINF_1:106

for X, Y being non empty Subset of ExtREAL holds inf (X \/ Y) = inf {(inf X),(inf Y)}

proof end;

theorem :: SUPINF_1:107

for X, Y, S being non empty Subset of ExtREAL st S = X /\ Y holds
sup S <=' inf {(sup X),(sup Y)}

proof end;

theorem :: SUPINF_1:108

for X, Y, S being non empty Subset of ExtREAL st S = X /\ Y holds
sup {(inf X),(inf Y)} <=' inf S

proof end;

definition

let X be non empty set ;
mode bool_DOMAIN of X -> set means :Def18: :: SUPINF_1:def 18
( it is non empty Subset-Family of X & ( for A being set st A in it holds
A is non empty set ) );
existence

proof end;

end;

:: deftheorem Def18 defines bool_DOMAIN SUPINF_1:def 18 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines SUP SUPINF_1:def 19 :

registration

let F be bool_DOMAIN of ExtREAL ;
cluster SUP F -> non empty ;
coherence

proof end;

end;

theorem :: SUPINF_1:109

canceled;

theorem :: SUPINF_1:110

canceled;

theorem :: SUPINF_1:111

canceled;

theorem Th112: :: SUPINF_1:112

for F being bool_DOMAIN of ExtREAL
for S being non empty Subset of ExtREAL st S = union F holds
sup S is majorant of SUP F

proof end;

theorem Th113: :: SUPINF_1:113

for F being bool_DOMAIN of ExtREAL
for S being Subset of ExtREAL st S = union F holds
sup (SUP F) is majorant of S

proof end;

theorem :: SUPINF_1:114

for F being bool_DOMAIN of ExtREAL
for S being non empty Subset of ExtREAL st S = union F holds
sup S = sup (SUP F)

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines INF SUPINF_1:def 20 :

registration

let F be bool_DOMAIN of ExtREAL ;
cluster INF F -> non empty ;
coherence

proof end;

end;

theorem :: SUPINF_1:115

canceled;

theorem :: SUPINF_1:116

canceled;

theorem Th117: :: SUPINF_1:117

for F being bool_DOMAIN of ExtREAL
for S being non empty Subset of ExtREAL st S = union F holds
inf S is minorant of INF F

proof end;

theorem Th118: :: SUPINF_1:118

for F being bool_DOMAIN of ExtREAL
for S being Subset of ExtREAL st S = union F holds
inf (INF F) is minorant of S

proof end;

theorem :: SUPINF_1:119

for F being bool_DOMAIN of ExtREAL
for S being non empty Subset of ExtREAL st S = union F holds
inf S = inf (INF F)

proof end;

theorem :: SUPINF_1:120

for x, y being R_eal
for p, q being real number st x = p & y = q holds
( p <= q iff x <=' y )

proof end;