XXREAL_2: Suprema and Infima of Intervals of Extended Real Numbers

:: Suprema and Infima of Intervals of Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received June 26, 2008
:: Copyright (c) 2008-2015 Association of Mizar Users

scheme :: XXREAL_2:sch 1
FinInter{ F₁() -> Integer, F₂() -> Integer, F₃( object ) -> object , P₁[ object ] } :

{ F₃(i) where i is Element of INT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite

proof end;

definition

let X be ext-real-membered set ;

mode UpperBound of X -> ExtReal means :Def1: :: XXREAL_2:def 1
for x being ExtReal st x in X holds
x <= it;

existence

proof end;

mode LowerBound of X -> ExtReal means :Def2: :: XXREAL_2:def 2
for x being ExtReal st x in X holds
it <= x;

existence

proof end;

end;

:: deftheorem Def1 defines UpperBound XXREAL_2:def 1 :

:: deftheorem Def2 defines LowerBound XXREAL_2:def 2 :

definition

let X be ext-real-membered set ;

func sup X -> ExtReal means :Def3: :: XXREAL_2:def 3
( it is UpperBound of X & ( for x being UpperBound of X holds it <= x ) );

existence

proof end;

uniqueness

proof end;

func inf X -> ExtReal means :Def4: :: XXREAL_2:def 4
( it is LowerBound of X & ( for x being LowerBound of X holds x <= it ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines sup XXREAL_2:def 3 :

:: deftheorem Def4 defines inf XXREAL_2:def 4 :

definition

let X be ext-real-membered set ;

attr X is left_end means :Def5: :: XXREAL_2:def 5
inf X in X;

attr X is right_end means :Def6: :: XXREAL_2:def 6
sup X in X;

end;

:: deftheorem Def5 defines left_end XXREAL_2:def 5 :

:: deftheorem Def6 defines right_end XXREAL_2:def 6 :

theorem Th1: :: XXREAL_2:1

for x, y being ExtReal holds
( y is UpperBound of {x} iff x <= y )

proof end;

theorem Th2: :: XXREAL_2:2

for x, y being ExtReal holds
( y is LowerBound of {x} iff y <= x )

proof end;

Lm1: for x being ExtReal holds sup {x} = x

proof end;

Lm2: for x being ExtReal holds inf {x} = x

proof end;

registration

cluster -> ext-real-membered for Element of Fin ExtREAL;

coherence

proof end;

end;

theorem Th3: :: XXREAL_2:3

for x being ExtReal
for A being ext-real-membered set st x in A holds
inf A <= x

proof end;

theorem Th4: :: XXREAL_2:4

for x being ExtReal
for A being ext-real-membered set st x in A holds
x <= sup A

proof end;

theorem Th5: :: XXREAL_2:5

for A, B being ext-real-membered set st B c= A holds
for x being LowerBound of A holds x is LowerBound of B

proof end;

theorem Th6: :: XXREAL_2:6

for A, B being ext-real-membered set st B c= A holds
for x being UpperBound of A holds x is UpperBound of B

proof end;

theorem Th7: :: XXREAL_2:7

for A, B being ext-real-membered set
for x being LowerBound of A
for y being LowerBound of B holds min (x,y) is LowerBound of A \/ B

proof end;

theorem Th8: :: XXREAL_2:8

for A, B being ext-real-membered set
for x being UpperBound of A
for y being UpperBound of B holds max (x,y) is UpperBound of A \/ B

proof end;

theorem Th9: :: XXREAL_2:9

for A, B being ext-real-membered set holds inf (A \/ B) = min ((inf A),(inf B))

proof end;

theorem Th10: :: XXREAL_2:10

for A, B being ext-real-membered set holds sup (A \/ B) = max ((sup A),(sup B))

proof end;

registration

cluster ext-real-membered finite non empty -> ext-real-membered non empty left_end right_end for set ;

coherence

proof end;

end;

registration

cluster natural-membered non empty -> natural-membered non empty left_end for set ;

coherence

proof end;

end;

registration

cluster complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty left_end right_end for set ;

existence

proof end;

end;

notation

let X be ext-real-membered left_end set ;
synonym min X for inf X;

end;

notation

let X be ext-real-membered right_end set ;
synonym max X for sup X;

end;

definition

let X be ext-real-membered left_end set ;

redefine func inf X means :Def7: :: XXREAL_2:def 7
( it in X & ( for x being ExtReal st x in X holds
it <= x ) );

compatibility

proof end;

end;

:: deftheorem Def7 defines inf XXREAL_2:def 7 :

definition

let X be ext-real-membered right_end set ;

redefine func sup X means :Def8: :: XXREAL_2:def 8
( it in X & ( for x being ExtReal st x in X holds
x <= it ) );

compatibility

proof end;

end;

:: deftheorem Def8 defines sup XXREAL_2:def 8 :

theorem :: XXREAL_2:11

for x being ExtReal holds max {x} = x by Lm1;

Lm3: for x, y being ExtReal st x <= y holds
y is UpperBound of {x,y}

proof end;

Lm4: for x, y being ExtReal
for z being UpperBound of {x,y} holds y <= z

proof end;

theorem :: XXREAL_2:12

for x, y being ExtReal holds max (x,y) = max {x,y}

proof end;

theorem :: XXREAL_2:13

for x being ExtReal holds min {x} = x by Lm2;

Lm5: for x, y being ExtReal st y <= x holds
y is LowerBound of {x,y}

proof end;

Lm6: for x, y being ExtReal
for z being LowerBound of {x,y} holds z <= y

proof end;

theorem :: XXREAL_2:14

for x, y being ExtReal holds min {x,y} = min (x,y)

proof end;

definition

let X be ext-real-membered set ;

attr X is bounded_below means :Def9: :: XXREAL_2:def 9
ex r being Real st r is LowerBound of X;

attr X is bounded_above means :Def10: :: XXREAL_2:def 10
ex r being Real st r is UpperBound of X;

end;

:: deftheorem Def9 defines bounded_below XXREAL_2:def 9 :

:: deftheorem Def10 defines bounded_above XXREAL_2:def 10 :

registration

cluster natural-membered finite non empty for set ;

existence

proof end;

end;

definition

let X be ext-real-membered set ;

attr X is real-bounded means :: XXREAL_2:def 11
( X is bounded_below & X is bounded_above );

end;

:: deftheorem defines real-bounded XXREAL_2:def 11 :

registration

cluster ext-real-membered real-bounded -> ext-real-membered bounded_below bounded_above for set ;

coherence ;

cluster ext-real-membered bounded_below bounded_above -> ext-real-membered real-bounded for set ;

coherence ;

end;

registration

cluster real-membered finite -> real-membered real-bounded for set ;

coherence

proof end;

end;

registration

cluster complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty left_end real-bounded for set ;

existence

proof end;

end;

theorem Th15: :: XXREAL_2:15

for X being real-membered non empty set st X is bounded_below holds
inf X in REAL

proof end;

theorem Th16: :: XXREAL_2:16

for X being real-membered non empty set st X is bounded_above holds
sup X in REAL

proof end;

registration

let X be real-membered non empty bounded_above set ;

cluster sup X -> real ;

coherence

proof end;

end;

registration

let X be real-membered non empty bounded_below set ;

cluster inf X -> real ;

coherence

proof end;

end;

registration

cluster integer-membered non empty bounded_above -> integer-membered non empty right_end for set ;

coherence

proof end;

end;

registration

cluster integer-membered non empty bounded_below -> integer-membered non empty left_end for set ;

coherence

proof end;

end;

registration

cluster natural-membered -> natural-membered bounded_below for set ;

coherence

proof end;

end;

registration

let X be real-membered left_end set ;

cluster inf X -> real ;

coherence

proof end;

end;

registration

let X be rational-membered left_end set ;

cluster inf X -> rational ;

coherence

proof end;

end;

registration

let X be integer-membered left_end set ;

cluster inf X -> integer ;

coherence

proof end;

end;

registration

let X be natural-membered left_end set ;

cluster inf X -> natural ;

coherence

proof end;

end;

registration

let X be real-membered right_end set ;

cluster sup X -> real ;

coherence

proof end;

end;

registration

let X be rational-membered right_end set ;

cluster sup X -> rational ;

coherence

proof end;

end;

registration

let X be integer-membered right_end set ;

cluster sup X -> integer ;

coherence

proof end;

end;

registration

let X be natural-membered right_end set ;

cluster sup X -> natural ;

coherence

proof end;

end;

registration

cluster real-membered left_end -> real-membered bounded_below for set ;

coherence

proof end;

cluster real-membered right_end -> real-membered bounded_above for set ;

coherence

proof end;

end;

theorem Th17: :: XXREAL_2:17

for x, y being ExtReal holds x is LowerBound of [.x,y.]

proof end;

theorem Th18: :: XXREAL_2:18

for x, y being ExtReal holds x is LowerBound of ].x,y.]

proof end;

theorem Th19: :: XXREAL_2:19

for x, y being ExtReal holds x is LowerBound of [.x,y.[

proof end;

theorem Th20: :: XXREAL_2:20

for x, y being ExtReal holds x is LowerBound of ].x,y.[

proof end;

theorem Th21: :: XXREAL_2:21

for x, y being ExtReal holds y is UpperBound of [.x,y.]

proof end;

theorem Th22: :: XXREAL_2:22

for x, y being ExtReal holds y is UpperBound of ].x,y.]

proof end;

theorem Th23: :: XXREAL_2:23

for x, y being ExtReal holds y is UpperBound of [.x,y.[

proof end;

theorem Th24: :: XXREAL_2:24

for x, y being ExtReal holds y is UpperBound of ].x,y.[

proof end;

theorem Th25: :: XXREAL_2:25

for x, y being ExtReal st x <= y holds
inf [.x,y.] = x

proof end;

theorem Th26: :: XXREAL_2:26

for x, y being ExtReal st x < y holds
inf [.x,y.[ = x

proof end;

theorem Th27: :: XXREAL_2:27

for x, y being ExtReal st x < y holds
inf ].x,y.] = x

proof end;

theorem Th28: :: XXREAL_2:28

for x, y being ExtReal st x < y holds
inf ].x,y.[ = x

proof end;

theorem Th29: :: XXREAL_2:29

for x, y being ExtReal st x <= y holds
sup [.x,y.] = y

proof end;

theorem Th30: :: XXREAL_2:30

for x, y being ExtReal st x < y holds
sup ].x,y.] = y

proof end;

theorem Th31: :: XXREAL_2:31

for x, y being ExtReal st x < y holds
sup [.x,y.[ = y

proof end;

theorem Th32: :: XXREAL_2:32

for x, y being ExtReal st x < y holds
sup ].x,y.[ = y

proof end;

theorem Th33: :: XXREAL_2:33

for x, y being ExtReal st x <= y holds
( [.x,y.] is left_end & [.x,y.] is right_end )

proof end;

theorem Th34: :: XXREAL_2:34

for x, y being ExtReal st x < y holds
[.x,y.[ is left_end

proof end;

theorem Th35: :: XXREAL_2:35

for x, y being ExtReal st x < y holds
].x,y.] is right_end

proof end;

theorem Th36: :: XXREAL_2:36

for x being ExtReal holds x is LowerBound of {}

proof end;

theorem Th37: :: XXREAL_2:37

for x being ExtReal holds x is UpperBound of {}

proof end;

theorem Th38: :: XXREAL_2:38

inf {} = +infty

proof end;

theorem Th39: :: XXREAL_2:39

sup {} = -infty

proof end;

theorem Th40: :: XXREAL_2:40

for X being ext-real-membered set holds
( not X is empty iff inf X <= sup X )

proof end;

registration

cluster integer-membered real-bounded -> integer-membered finite for set ;

coherence

proof end;

end;

registration

cluster natural-membered bounded_above -> natural-membered finite bounded_above for set ;

coherence ;

end;

theorem :: XXREAL_2:41

for X being ext-real-membered set holds +infty is UpperBound of X

proof end;

theorem :: XXREAL_2:42

for X being ext-real-membered set holds -infty is LowerBound of X

proof end;

theorem Th43: :: XXREAL_2:43

for X, Y being ext-real-membered set st X c= Y & Y is bounded_above holds
X is bounded_above

proof end;

theorem Th44: :: XXREAL_2:44

for X, Y being ext-real-membered set st X c= Y & Y is bounded_below holds
X is bounded_below

proof end;

theorem :: XXREAL_2:45

for X, Y being ext-real-membered set st X c= Y & Y is real-bounded holds
X is real-bounded by Th43, Th44;

theorem Th46: :: XXREAL_2:46

( not REAL is bounded_below & not REAL is bounded_above )

proof end;

registration

cluster REAL -> non bounded_below non bounded_above ;

coherence by Th46;

end;

theorem :: XXREAL_2:47

{+infty} is bounded_below

proof end;

theorem :: XXREAL_2:48

{-infty} is bounded_above

proof end;

theorem Th49: :: XXREAL_2:49

for X being ext-real-membered non empty bounded_above set st X <> {-infty} holds
ex x being Element of REAL st x in X

proof end;

theorem Th50: :: XXREAL_2:50

for X being ext-real-membered non empty bounded_below set st X <> {+infty} holds
ex x being Element of REAL st x in X

proof end;

theorem Th51: :: XXREAL_2:51

for X being ext-real-membered set st -infty is UpperBound of X holds
X c= {-infty}

proof end;

theorem Th52: :: XXREAL_2:52

for X being ext-real-membered set st +infty is LowerBound of X holds
X c= {+infty}

proof end;

theorem :: XXREAL_2:53

for X being ext-real-membered non empty set st ex y being UpperBound of X st y <> +infty holds
X is bounded_above

proof end;

theorem :: XXREAL_2:54

for X being ext-real-membered non empty set st ex y being LowerBound of X st y <> -infty holds
X is bounded_below

proof end;

theorem :: XXREAL_2:55

for X being ext-real-membered non empty set
for x being UpperBound of X st x in X holds
x = sup X

proof end;

theorem :: XXREAL_2:56

for X being ext-real-membered non empty set
for x being LowerBound of X st x in X holds
x = inf X

proof end;

theorem Th57: :: XXREAL_2:57

for X being ext-real-membered non empty set st X is bounded_above & X <> {-infty} holds
sup X in REAL

proof end;

theorem Th58: :: XXREAL_2:58

for X being ext-real-membered non empty set st X is bounded_below & X <> {+infty} holds
inf X in REAL

proof end;

theorem :: XXREAL_2:59

for X, Y being ext-real-membered set st X c= Y holds
sup X <= sup Y

proof end;

theorem :: XXREAL_2:60

for X, Y being ext-real-membered set st X c= Y holds
inf Y <= inf X

proof end;

theorem :: XXREAL_2:61

for X being ext-real-membered set
for x being ExtReal st ex y being ExtReal st
( y in X & x <= y ) holds
x <= sup X

proof end;

theorem :: XXREAL_2:62

for X being ext-real-membered set
for x being ExtReal st ex y being ExtReal st
( y in X & y <= x ) holds
inf X <= x

proof end;

theorem :: XXREAL_2:63

for X, Y being ext-real-membered set st ( for x being ExtReal st x in X holds
ex y being ExtReal st
( y in Y & x <= y ) ) holds
sup X <= sup Y

proof end;

theorem :: XXREAL_2:64

for X, Y being ext-real-membered set st ( for y being ExtReal st y in Y holds
ex x being ExtReal st
( x in X & x <= y ) ) holds
inf X <= inf Y

proof end;

theorem Th65: :: XXREAL_2:65

for X, Y being ext-real-membered set
for x being UpperBound of X
for y being UpperBound of Y holds min (x,y) is UpperBound of X /\ Y

proof end;

theorem Th66: :: XXREAL_2:66

for X, Y being ext-real-membered set
for x being LowerBound of X
for y being LowerBound of Y holds max (x,y) is LowerBound of X /\ Y

proof end;

theorem :: XXREAL_2:67

for X, Y being ext-real-membered set holds sup (X /\ Y) <= min ((sup X),(sup Y))

proof end;

theorem :: XXREAL_2:68

for X, Y being ext-real-membered set holds max ((inf X),(inf Y)) <= inf (X /\ Y)

proof end;

registration

cluster ext-real-membered real-bounded -> ext-real-membered real-membered for set ;

coherence

proof end;

end;

theorem Th69: :: XXREAL_2:69

for A being ext-real-membered set holds A c= [.(inf A),(sup A).]

proof end;

theorem :: XXREAL_2:70

for A being ext-real-membered set st sup A = inf A holds
A = {(inf A)}

proof end;

theorem Th71: :: XXREAL_2:71

for x, y being ExtReal
for A being ext-real-membered set st x <= y & x is UpperBound of A holds
y is UpperBound of A

proof end;

theorem Th72: :: XXREAL_2:72

for x, y being ExtReal
for A being ext-real-membered set st y <= x & x is LowerBound of A holds
y is LowerBound of A

proof end;

theorem :: XXREAL_2:73

for A being ext-real-membered set holds
( A is bounded_above iff sup A <> +infty )

proof end;

theorem :: XXREAL_2:74

for A being ext-real-membered set holds
( A is bounded_below iff inf A <> -infty )

proof end;

definition

let A be ext-real-membered set ;

attr A is interval means :Def12: :: XXREAL_2:def 12
for r, s being ExtReal st r in A & s in A holds
[.r,s.] c= A;

end;

:: deftheorem Def12 defines interval XXREAL_2:def 12 :

registration

cluster ExtREAL -> interval ;

coherence by MEMBERED:2;

cluster ext-real-membered empty -> ext-real-membered interval for set ;

coherence ;
let r, s be ExtReal;

cluster [.r,s.] -> interval ;

coherence

proof end;

cluster ].r,s.] -> interval ;

coherence

proof end;

cluster [.r,s.[ -> interval ;

coherence

proof end;

cluster ].r,s.[ -> interval ;

coherence

proof end;

end;

registration

cluster REAL -> interval ;

coherence by XXREAL_1:224;

end;

registration

cluster ext-real-membered non empty interval for set ;

existence

proof end;

end;

registration

let A, B be ext-real-membered interval set ;

cluster A /\ B -> interval ;

coherence

proof end;

end;

registration

let r, s be ExtReal;

cluster ].r,s.] -> non left_end ;

coherence

proof end;

cluster [.r,s.[ -> non right_end ;

coherence

proof end;

cluster ].r,s.[ -> non left_end non right_end ;

coherence

proof end;

end;

registration

cluster ext-real-membered left_end right_end interval for set ;

existence

proof end;

cluster ext-real-membered non left_end right_end interval for set ;

existence

proof end;

cluster ext-real-membered left_end non right_end interval for set ;

existence

proof end;

cluster ext-real-membered non empty non left_end non right_end interval for set ;

existence

proof end;

end;

theorem :: XXREAL_2:75

for A being ext-real-membered left_end right_end interval set holds A = [.(min A),(max A).]

proof end;

theorem :: XXREAL_2:76

for A being ext-real-membered non left_end right_end interval set holds A = ].(inf A),(max A).]

proof end;

theorem :: XXREAL_2:77

for A being ext-real-membered left_end non right_end interval set holds A = [.(min A),(sup A).[

proof end;

theorem Th78: :: XXREAL_2:78

for A being ext-real-membered non empty non left_end non right_end interval set holds A = ].(inf A),(sup A).[

proof end;

theorem :: XXREAL_2:79

for A being ext-real-membered non left_end non right_end interval set ex r, s being ExtReal st
( r <= s & A = ].r,s.[ )

proof end;

theorem Th80: :: XXREAL_2:80

for A being ext-real-membered set st A is interval holds
for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds
r in A

proof end;

theorem Th81: :: XXREAL_2:81

for A being ext-real-membered set st A is interval holds
for x, r being ExtReal st x in A & x <= r & r < sup A holds
r in A

proof end;

theorem Th82: :: XXREAL_2:82

for A being ext-real-membered set st A is interval holds
for x, r being ExtReal st x in A & inf A < r & r <= x holds
r in A

proof end;

theorem :: XXREAL_2:83

for A being ext-real-membered set st A is interval holds
for r being ExtReal st inf A < r & r < sup A holds
r in A

proof end;

theorem Th84: :: XXREAL_2:84

for A being ext-real-membered set st ( for x, y, r being ExtReal st x in A & y in A & x < r & r < y holds
r in A ) holds
A is interval

proof end;

theorem :: XXREAL_2:85

for A being ext-real-membered set st ( for x, r being ExtReal st x in A & x < r & r < sup A holds
r in A ) holds
A is interval

proof end;

theorem :: XXREAL_2:86

for A being ext-real-membered set st ( for y, r being ExtReal st y in A & inf A < r & r < y holds
r in A ) holds
A is interval

proof end;

theorem :: XXREAL_2:87

for A being ext-real-membered set st ( for r being ExtReal st inf A < r & r < sup A holds
r in A ) holds
A is interval

proof end;

theorem Th88: :: XXREAL_2:88

for A being ext-real-membered set st ( for x, y, r being ExtReal st x in A & y in A & x <= r & r <= y holds
r in A ) holds
A is interval

proof end;

theorem :: XXREAL_2:89

for A, B being ext-real-membered set st A is interval & B is interval & A meets B holds
A \/ B is interval

proof end;

theorem :: XXREAL_2:90

for A, B being ext-real-membered set st A is interval & B is left_end & B is interval & sup A = inf B holds
A \/ B is interval

proof end;

theorem :: XXREAL_2:91

for A, B being ext-real-membered set st A is right_end & A is interval & B is interval & sup A = inf B holds
A \/ B is interval

proof end;

registration

cluster ext-real-membered left_end -> ext-real-membered non empty for set ;

coherence ;

cluster ext-real-membered right_end -> ext-real-membered non empty for set ;

coherence ;

end;

:: from HAHNBAN, 2011.04.26, A.T.

theorem :: XXREAL_2:92

for A being non empty Subset of ExtREAL st ( for r being Element of ExtREAL st r in A holds
r <= -infty ) holds
A = {-infty}

proof end;

theorem :: XXREAL_2:93

for A being non empty Subset of ExtREAL st ( for r being Element of ExtREAL st r in A holds
+infty <= r ) holds
A = {+infty}

proof end;

theorem Th94: :: XXREAL_2:94

for A being non empty Subset of ExtREAL
for r being ExtReal st r < sup A holds
ex s being Element of ExtREAL st
( s in A & r < s )

proof end;

theorem Th95: :: XXREAL_2:95

for A being non empty Subset of ExtREAL
for r being Element of ExtREAL st inf A < r holds
ex s being Element of ExtREAL st
( s in A & s < r )

proof end;

theorem :: XXREAL_2:96

for A, B being non empty Subset of ExtREAL st ( for r, s being ExtReal st r in A & s in B holds
r <= s ) holds
sup A <= inf B

proof end;