:: by Andrzej Trybulec

::

:: Received June 26, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

definition

let X be ext-real-membered set ;

ex b_{1} being ext-real number st

for x being ext-real number st x in X holds

x <= b_{1}

ex b_{1} being ext-real number st

for x being ext-real number st x in X holds

b_{1} <= x

end;
mode UpperBound of X -> ext-real number means :Def1: :: XXREAL_2:def 1

for x being ext-real number st x in X holds

x <= it;

existence for x being ext-real number st x in X holds

x <= it;

ex b

for x being ext-real number st x in X holds

x <= b

proof end;

mode LowerBound of X -> ext-real number means :Def2: :: XXREAL_2:def 2

for x being ext-real number st x in X holds

it <= x;

existence for x being ext-real number st x in X holds

it <= x;

ex b

for x being ext-real number st x in X holds

b

proof end;

:: deftheorem Def1 defines UpperBound XXREAL_2:def 1 :

for X being ext-real-membered set

for b_{2} being ext-real number holds

( b_{2} is UpperBound of X iff for x being ext-real number st x in X holds

x <= b_{2} );

for X being ext-real-membered set

for b

( b

x <= b

:: deftheorem Def2 defines LowerBound XXREAL_2:def 2 :

for X being ext-real-membered set

for b_{2} being ext-real number holds

( b_{2} is LowerBound of X iff for x being ext-real number st x in X holds

b_{2} <= x );

for X being ext-real-membered set

for b

( b

b

definition

let X be ext-real-membered set ;

ex b_{1} being ext-real number st

( b_{1} is UpperBound of X & ( for x being UpperBound of X holds b_{1} <= x ) )

for b_{1}, b_{2} being ext-real number st b_{1} is UpperBound of X & ( for x being UpperBound of X holds b_{1} <= x ) & b_{2} is UpperBound of X & ( for x being UpperBound of X holds b_{2} <= x ) holds

b_{1} = b_{2}

ex b_{1} being ext-real number st

( b_{1} is LowerBound of X & ( for x being LowerBound of X holds x <= b_{1} ) )

for b_{1}, b_{2} being ext-real number st b_{1} is LowerBound of X & ( for x being LowerBound of X holds x <= b_{1} ) & b_{2} is LowerBound of X & ( for x being LowerBound of X holds x <= b_{2} ) holds

b_{1} = b_{2}

end;
func sup X -> ext-real number means :Def3: :: XXREAL_2:def 3

( it is UpperBound of X & ( for x being UpperBound of X holds it <= x ) );

existence ( it is UpperBound of X & ( for x being UpperBound of X holds it <= x ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

func inf X -> ext-real number means :Def4: :: XXREAL_2:def 4

( it is LowerBound of X & ( for x being LowerBound of X holds x <= it ) );

existence ( it is LowerBound of X & ( for x being LowerBound of X holds x <= it ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines sup XXREAL_2:def 3 :

for X being ext-real-membered set

for b_{2} being ext-real number holds

( b_{2} = sup X iff ( b_{2} is UpperBound of X & ( for x being UpperBound of X holds b_{2} <= x ) ) );

for X being ext-real-membered set

for b

( b

:: deftheorem Def4 defines inf XXREAL_2:def 4 :

for X being ext-real-membered set

for b_{2} being ext-real number holds

( b_{2} = inf X iff ( b_{2} is LowerBound of X & ( for x being LowerBound of X holds x <= b_{2} ) ) );

for X being ext-real-membered set

for b

( b

:: deftheorem Def5 defines left_end XXREAL_2:def 5 :

for X being ext-real-membered set holds

( X is left_end iff inf X in X );

for X being ext-real-membered set holds

( X is left_end iff inf X in X );

:: deftheorem Def6 defines right_end XXREAL_2:def 6 :

for X being ext-real-membered set holds

( X is right_end iff sup X in X );

for X being ext-real-membered set holds

( X is right_end iff sup X in X );

Lm1: for x being ext-real number holds sup {x} = x

proof end;

Lm2: for x being ext-real number holds inf {x} = x

proof end;

registration
end;

theorem Th5: :: XXREAL_2:5

for B, A being ext-real-membered set st B c= A holds

for x being LowerBound of A holds x is LowerBound of B

for x being LowerBound of A holds x is LowerBound of B

proof end;

theorem Th6: :: XXREAL_2:6

for B, A being ext-real-membered set st B c= A holds

for x being UpperBound of A holds x is UpperBound of B

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

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

for x being UpperBound of A

for y being UpperBound of B holds max (x,y) is UpperBound of A \/ B

proof end;

registration

for b_{1} being ext-real-membered non empty set st b_{1} is finite holds

( b_{1} is left_end & b_{1} is right_end )
end;

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

coherence for b

( b

proof end;

registration
end;

registration

ex b_{1} being natural-membered non empty set st b_{1} is right_end
end;

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

existence ex b

proof end;

definition

let X be ext-real-membered left_end set ;

for b_{1} being ext-real number holds

( b_{1} = inf X iff ( b_{1} in X & ( for x being ext-real number st x in X holds

b_{1} <= x ) ) )

end;
redefine func inf X means :Def7: :: XXREAL_2:def 7

( it in X & ( for x being ext-real number st x in X holds

it <= x ) );

compatibility ( it in X & ( for x being ext-real number st x in X holds

it <= x ) );

for b

( b

b

proof end;

:: deftheorem Def7 defines inf XXREAL_2:def 7 :

for X being ext-real-membered left_end set

for b_{2} being ext-real number holds

( b_{2} = inf X iff ( b_{2} in X & ( for x being ext-real number st x in X holds

b_{2} <= x ) ) );

for X being ext-real-membered left_end set

for b

( b

b

definition

let X be ext-real-membered right_end set ;

for b_{1} being ext-real number holds

( b_{1} = sup X iff ( b_{1} in X & ( for x being ext-real number st x in X holds

x <= b_{1} ) ) )

end;
redefine func sup X means :Def8: :: XXREAL_2:def 8

( it in X & ( for x being ext-real number st x in X holds

x <= it ) );

compatibility ( it in X & ( for x being ext-real number st x in X holds

x <= it ) );

for b

( b

x <= b

proof end;

:: deftheorem Def8 defines sup XXREAL_2:def 8 :

for X being ext-real-membered right_end set

for b_{2} being ext-real number holds

( b_{2} = sup X iff ( b_{2} in X & ( for x being ext-real number st x in X holds

x <= b_{2} ) ) );

for X being ext-real-membered right_end set

for b

( b

x <= b

Lm3: for x, y being ext-real number st x <= y holds

y is UpperBound of {x,y}

proof end;

Lm4: for x, y being ext-real number

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

proof end;

Lm5: for y, x being ext-real number st y <= x holds

y is LowerBound of {x,y}

proof end;

Lm6: for x, y being ext-real number

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

proof end;

definition

let X be ext-real-membered set ;

end;
attr X is bounded_below means :Def9: :: XXREAL_2:def 9

ex r being real number st r is LowerBound of X;

ex r being real number st r is LowerBound of X;

attr X is bounded_above means :Def10: :: XXREAL_2:def 10

ex r being real number st r is UpperBound of X;

ex r being real number st r is UpperBound of X;

:: deftheorem Def9 defines bounded_below XXREAL_2:def 9 :

for X being ext-real-membered set holds

( X is bounded_below iff ex r being real number st r is LowerBound of X );

for X being ext-real-membered set holds

( X is bounded_below iff ex r being real number st r is LowerBound of X );

:: deftheorem Def10 defines bounded_above XXREAL_2:def 10 :

for X being ext-real-membered set holds

( X is bounded_above iff ex r being real number st r is UpperBound of X );

for X being ext-real-membered set holds

( X is bounded_above iff ex r being real number st r is UpperBound of X );

registration

existence

ex b_{1} being set st

( not b_{1} is empty & b_{1} is finite & b_{1} is natural-membered )

end;
ex b

( not b

proof end;

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

for X being ext-real-membered set holds

( X is real-bounded iff ( X is bounded_below & X is bounded_above ) );

for X being ext-real-membered set holds

( X is real-bounded iff ( X is bounded_below & X is bounded_above ) );

registration

coherence

for b_{1} being ext-real-membered set st b_{1} is real-bounded holds

( b_{1} is bounded_above & b_{1} is bounded_below )
by Def11;

coherence

for b_{1} being ext-real-membered set st b_{1} is bounded_above & b_{1} is bounded_below holds

b_{1} is real-bounded
by Def11;

end;
for b

( b

coherence

for b

b

registration

coherence

for b_{1} being real-membered set st b_{1} is finite holds

b_{1} is real-bounded

end;
for b

b

proof end;

registration

ex b_{1} being natural-membered non empty set st b_{1} is real-bounded
end;

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

existence ex b

proof end;

registration
end;

registration
end;

registration

coherence

for b_{1} being integer-membered non empty set st b_{1} is bounded_above holds

b_{1} is right_end

end;
for b

b

proof end;

registration

coherence

for b_{1} being integer-membered non empty set st b_{1} is bounded_below holds

b_{1} is left_end

end;
for b

b

proof end;

registration
end;

registration

coherence

for b_{1} being real-membered set st b_{1} is left_end holds

b_{1} is bounded_below

for b_{1} being real-membered set st b_{1} is right_end holds

b_{1} is bounded_above

end;
for b

b

proof end;

coherence for b

b

proof end;

registration

coherence

for b_{1} being integer-membered set st b_{1} is real-bounded holds

b_{1} is finite

end;
for b

b

proof end;

registration
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

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

ex x being Element of REAL st x in X

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

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

X is bounded_below

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

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

inf X in REAL

proof end;

theorem :: XXREAL_2:61

for X being ext-real-membered set

for x being ext-real number st ex y being ext-real number st

( y in X & x <= y ) holds

x <= sup X

for x being ext-real number st ex y being ext-real number 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 ext-real number st ex y being ext-real number st

( y in X & y <= x ) holds

inf X <= x

for x being ext-real number st ex y being ext-real number 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 ext-real number st x in X holds

ex y being ext-real number st

( y in Y & x <= y ) ) holds

sup X <= sup Y

ex y being ext-real number 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 ext-real number st y in Y holds

ex x being ext-real number st

( x in X & x <= y ) ) holds

inf X <= inf Y

ex x being ext-real number 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

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

for x being LowerBound of X

for y being LowerBound of Y holds max (x,y) is LowerBound of X /\ Y

proof end;

registration

coherence

for b_{1} being ext-real-membered set st b_{1} is real-bounded holds

b_{1} is real-membered

end;
for b

b

proof end;

theorem Th71: :: XXREAL_2:71

for x, y being ext-real number

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

y is UpperBound of A

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 y, x being ext-real number

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

y is LowerBound of A

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

y is LowerBound of A

proof end;

begin

:: deftheorem Def12 defines interval XXREAL_2:def 12 :

for A being ext-real-membered set holds

( A is interval iff for r, s being ext-real number st r in A & s in A holds

[.r,s.] c= A );

for A being ext-real-membered set holds

( A is interval iff for r, s being ext-real number st r in A & s in A holds

[.r,s.] c= A );

registration

coherence

ExtREAL is interval

for b_{1} being ext-real-membered set st b_{1} is empty holds

b_{1} is interval

coherence

[.r,s.] is interval

].r,s.] is interval

[.r,s.[ is interval

].r,s.[ is interval

end;
ExtREAL is interval

proof end;

coherence for b

b

proof end;

let r, s be ext-real number ;coherence

[.r,s.] is interval

proof end;

coherence ].r,s.] is interval

proof end;

coherence [.r,s.[ is interval

proof end;

coherence ].r,s.[ is interval

proof end;

registration
end;

registration
end;

registration

let r, s be ext-real number ;

coherence

not ].r,s.] is left_end

not [.r,s.[ is right_end

( not ].r,s.[ is left_end & not ].r,s.[ is right_end )

end;
coherence

not ].r,s.] is left_end

proof end;

coherence not [.r,s.[ is right_end

proof end;

coherence ( not ].r,s.[ is left_end & not ].r,s.[ is right_end )

proof end;

registration

existence

ex b_{1} being ext-real-membered set st

( b_{1} is left_end & b_{1} is right_end & b_{1} is interval )

ex b_{1} being ext-real-membered set st

( not b_{1} is left_end & b_{1} is right_end & b_{1} is interval )

ex b_{1} being ext-real-membered set st

( b_{1} is left_end & not b_{1} is right_end & b_{1} is interval )

ex b_{1} being ext-real-membered set st

( not b_{1} is left_end & not b_{1} is right_end & b_{1} is interval & not b_{1} is empty )

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

existence ex b

( b

proof end;

existence ex b

( not b

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 ext-real number st

( r <= s & A = ].r,s.[ )

( 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 ext-real number st x in A & y in A & x <= r & r <= y holds

r in A

for x, y, r being ext-real number 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 ext-real number st x in A & x <= r & r < sup A holds

r in A

for x, r being ext-real number 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 ext-real number st x in A & inf A < r & r <= x holds

r in A

for x, r being ext-real number 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 ext-real number st inf A < r & r < sup A holds

r in A

for r being ext-real number 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 ext-real number st x in A & y in A & x < r & r < y holds

r in A ) holds

A is interval

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 ext-real number st x in A & x < r & r < sup A holds

r in A ) holds

A is interval

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 ext-real number st y in A & inf A < r & r < y holds

r in A ) holds

A is interval

r in A ) holds

A is interval

proof end;

theorem :: XXREAL_2:87

for A being ext-real-membered set st ( for r being ext-real number st inf A < r & r < sup A holds

r in A ) holds

A is interval

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 ext-real number st x in A & y in A & x <= r & r <= y holds

r in A ) holds

A is interval

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

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

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

A \/ B is interval

proof end;

registration

coherence

for b_{1} being ext-real-membered set st b_{1} is left_end holds

not b_{1} is empty

for b_{1} being ext-real-membered set st b_{1} is right_end holds

not b_{1} is empty

end;
for b

not b

proof end;

coherence for b

not b

proof 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}

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}

+infty <= r ) holds

A = {+infty}

proof end;

theorem Th94: :: XXREAL_2:94

for A being non empty Subset of ExtREAL

for r being ext-real number st r < sup A holds

ex s being Element of ExtREAL st

( s in A & r < s )

for r being ext-real number 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 )

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 Element of ExtREAL st r in A & s in B holds

r <= s ) holds

sup A <= inf B

r <= s ) holds

sup A <= inf B

proof end;