:: by Library Committee

::

:: Received January 4, 2006

:: Copyright (c) 2006 Association of Mizar Users

begin

:: deftheorem Def1 defines ext-real XXREAL_0:def 1 :

for x being set holds

( x is ext-real iff x in ExtREAL );

registration

cluster ext-real set ;

existence

ex b_{1} being number st b_{1} is ext-real

coherence

for b_{1} being Element of ExtREAL holds b_{1} is ext-real
by Def1;

end;
existence

ex b

proof end;

cluster -> ext-real Element of ExtREAL ;coherence

for b

definition

func +infty -> set equals :: XXREAL_0:def 2

REAL ;

coherence

REAL is set ;

func -infty -> set equals :: XXREAL_0:def 3

[0,REAL];

coherence

[0,REAL] is set ;

end;
REAL ;

coherence

REAL is set ;

func -infty -> set equals :: XXREAL_0:def 3

[0,REAL];

coherence

[0,REAL] is set ;

:: deftheorem defines +infty XXREAL_0:def 2 :

+infty = REAL ;

:: deftheorem defines -infty XXREAL_0:def 3 :

-infty = [0,REAL];

definition

redefine func ExtREAL equals :: XXREAL_0:def 4

REAL \/ {+infty,-infty};

compatibility

for b_{1} being set holds

( b_{1} = ExtREAL iff b_{1} = REAL \/ {+infty,-infty} )
;

end;
REAL \/ {+infty,-infty};

compatibility

for b

( b

:: deftheorem defines ExtREAL XXREAL_0:def 4 :

ExtREAL = REAL \/ {+infty,-infty};

registration

cluster +infty -> ext-real ;

coherence

+infty is ext-real

coherence

-infty is ext-real

end;
coherence

+infty is ext-real

proof end;

cluster -infty -> ext-real ;coherence

-infty is ext-real

proof end;

definition

let x, y be ext-real number ;

pred x <= y means :Def5: :: XXREAL_0:def 5

ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & x9 <=' y9 ) if ( x in REAL+ & y in REAL+ )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] )

otherwise ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty );

consistency

( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & x9 <=' y9 ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) by ARYTM_0:5, XBOOLE_0:3;

reflexivity

for x being ext-real number holds

( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )

for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) holds

( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

end;
pred x <= y means :Def5: :: XXREAL_0:def 5

ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & x9 <=' y9 ) if ( x in REAL+ & y in REAL+ )

ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] )

otherwise ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty );

consistency

( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & x9 <=' y9 ) iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) by ARYTM_0:5, XBOOLE_0:3;

reflexivity

for x being ext-real number holds

( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )

proof end;

connectedness for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) holds

( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

proof end;

:: deftheorem Def5 defines <= XXREAL_0:def 5 :

for x, y being ext-real number holds

( ( x in REAL+ & y in REAL+ implies ( x <= y iff ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( x <= y iff ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( x <= y iff ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty ) ) ) );

notation

let a, b be ext-real number ;

synonym b >= a for a <= b;

antonym b < a for a <= b;

antonym a > b for a <= b;

end;
synonym b >= a for a <= b;

antonym b < a for a <= b;

antonym a > b for a <= b;

Lm1: +infty <> [0,0]

proof end;

Lm2: not +infty in REAL+

by ARYTM_0:1, ORDINAL1:7;

Lm3: not -infty in REAL+

proof end;

Lm4: not +infty in [:{0},REAL+:]

proof end;

Lm5: not -infty in [:{0},REAL+:]

proof end;

Lm6: -infty < +infty

proof end;

theorem Th1: :: XXREAL_0:1

proof end;

Lm7: for a being ext-real number st -infty >= a holds

a = -infty

proof end;

Lm8: for a being ext-real number st +infty <= a holds

a = +infty

proof end;

theorem Th2: :: XXREAL_0:2

proof end;

theorem :: XXREAL_0:3

theorem :: XXREAL_0:4

theorem :: XXREAL_0:5

theorem :: XXREAL_0:6

theorem :: XXREAL_0:7

theorem :: XXREAL_0:8

Lm9: for a being ext-real number holds

( a in REAL or a = +infty or a = -infty )

proof end;

theorem Th9: :: XXREAL_0:9

proof end;

theorem Th10: :: XXREAL_0:10

proof end;

theorem Th11: :: XXREAL_0:11

proof end;

theorem Th12: :: XXREAL_0:12

proof end;

theorem Th13: :: XXREAL_0:13

proof end;

theorem :: XXREAL_0:14

begin

registration

cluster natural -> ext-real set ;

coherence

for b_{1} being number st b_{1} is natural holds

b_{1} is ext-real

end;
coherence

for b

b

proof end;

definition

let a be ext-real number ;

attr a is positive means :: XXREAL_0:def 6

a > 0 ;

attr a is negative means :: XXREAL_0:def 7

a < 0 ;

redefine attr a is empty means :: XXREAL_0:def 8

a = 0 ;

compatibility

( a is zero iff a = 0 ) ;

end;
attr a is positive means :: XXREAL_0:def 6

a > 0 ;

attr a is negative means :: XXREAL_0:def 7

a < 0 ;

redefine attr a is empty means :: XXREAL_0:def 8

a = 0 ;

compatibility

( a is zero iff a = 0 ) ;

:: deftheorem defines positive XXREAL_0:def 6 :

for a being ext-real number holds

( a is positive iff a > 0 );

:: deftheorem defines negative XXREAL_0:def 7 :

for a being ext-real number holds

( a is negative iff a < 0 );

:: deftheorem defines zero XXREAL_0:def 8 :

for a being ext-real number holds

( a is zero iff a = 0 );

registration

cluster ext-real positive -> non zero ext-real non negative set ;

coherence

for b_{1} being ext-real number st b_{1} is positive holds

( not b_{1} is negative & not b_{1} is zero )

coherence

for b_{1} being ext-real number st not b_{1} is negative & not b_{1} is zero holds

b_{1} is positive

coherence

for b_{1} being ext-real number st b_{1} is negative holds

( not b_{1} is positive & not b_{1} is zero )

coherence

for b_{1} being ext-real number st not b_{1} is positive & not b_{1} is zero holds

b_{1} is negative
;

cluster zero ext-real -> ext-real non positive non negative set ;

coherence

for b_{1} being ext-real number st b_{1} is zero holds

( not b_{1} is negative & not b_{1} is positive )
;

cluster ext-real non positive non negative -> zero ext-real set ;

coherence

for b_{1} being ext-real number st not b_{1} is negative & not b_{1} is positive holds

b_{1} is zero
;

end;
coherence

for b

( not b

proof end;

cluster non zero ext-real non negative -> ext-real positive set ;coherence

for b

b

proof end;

cluster ext-real negative -> non zero ext-real non positive set ;coherence

for b

( not b

proof end;

cluster non zero ext-real non positive -> ext-real negative set ;coherence

for b

b

cluster zero ext-real -> ext-real non positive non negative set ;

coherence

for b

( not b

cluster ext-real non positive non negative -> zero ext-real set ;

coherence

for b

b

registration

cluster +infty -> positive ;

coherence

+infty is positive

coherence

-infty is negative

end;
coherence

+infty is positive

proof end;

cluster -infty -> negative ;coherence

-infty is negative

proof end;

registration

cluster ext-real positive set ;

existence

ex b_{1} being ext-real number st b_{1} is positive

existence

ex b_{1} being ext-real number st b_{1} is negative

existence

ex b_{1} being ext-real number st b_{1} is zero

end;
existence

ex b

proof end;

cluster ext-real negative set ;existence

ex b

proof end;

cluster zero ext-real set ;existence

ex b

proof end;

begin

definition

let a, b be ext-real number ;

func min (a,b) -> set equals :Def9: :: XXREAL_0:def 9

a if a <= b

otherwise b;

correctness

coherence

( ( a <= b implies a is set ) & ( not a <= b implies b is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being ext-real number st ( a <= b implies b_{1} = a ) & ( not a <= b implies b_{1} = b ) holds

( ( b <= a implies b_{1} = b ) & ( not b <= a implies b_{1} = a ) )
by Th1;

idempotence

for a being ext-real number holds

( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;

func max (a,b) -> set equals :Def10: :: XXREAL_0:def 10

a if b <= a

otherwise b;

correctness

coherence

( ( b <= a implies a is set ) & ( not b <= a implies b is set ) );

consistency

for b_{1} being set holds verum;

;

commutativity

for b_{1} being set

for a, b being ext-real number st ( b <= a implies b_{1} = a ) & ( not b <= a implies b_{1} = b ) holds

( ( a <= b implies b_{1} = b ) & ( not a <= b implies b_{1} = a ) )
by Th1;

idempotence

for a being ext-real number holds

( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;

end;
func min (a,b) -> set equals :Def9: :: XXREAL_0:def 9

a if a <= b

otherwise b;

correctness

coherence

( ( a <= b implies a is set ) & ( not a <= b implies b is set ) );

consistency

for b

;

commutativity

for b

for a, b being ext-real number st ( a <= b implies b

( ( b <= a implies b

idempotence

for a being ext-real number holds

( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;

func max (a,b) -> set equals :Def10: :: XXREAL_0:def 10

a if b <= a

otherwise b;

correctness

coherence

( ( b <= a implies a is set ) & ( not b <= a implies b is set ) );

consistency

for b

;

commutativity

for b

for a, b being ext-real number st ( b <= a implies b

( ( a <= b implies b

idempotence

for a being ext-real number holds

( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;

:: deftheorem Def9 defines min XXREAL_0:def 9 :

for a, b being ext-real number holds

( ( a <= b implies min (a,b) = a ) & ( not a <= b implies min (a,b) = b ) );

:: deftheorem Def10 defines max XXREAL_0:def 10 :

for a, b being ext-real number holds

( ( b <= a implies max (a,b) = a ) & ( not b <= a implies max (a,b) = b ) );

theorem :: XXREAL_0:15

theorem :: XXREAL_0:16

registration

let a, b be ext-real number ;

cluster min (a,b) -> ext-real ;

coherence

min (a,b) is ext-real by Def9;

cluster max (a,b) -> ext-real ;

coherence

max (a,b) is ext-real by Def10;

end;
cluster min (a,b) -> ext-real ;

coherence

min (a,b) is ext-real by Def9;

cluster max (a,b) -> ext-real ;

coherence

max (a,b) is ext-real by Def10;

theorem Th17: :: XXREAL_0:17

proof end;

theorem Th18: :: XXREAL_0:18

proof end;

theorem :: XXREAL_0:19

proof end;

theorem :: XXREAL_0:20

theorem :: XXREAL_0:21

theorem :: XXREAL_0:22

proof end;

theorem :: XXREAL_0:23

proof end;

theorem :: XXREAL_0:24

for c, a, b being ext-real number st c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds

d <= c ) holds

c = min (a,b)

d <= c ) holds

c = min (a,b)

proof end;

theorem Th25: :: XXREAL_0:25

proof end;

theorem Th26: :: XXREAL_0:26

proof end;

theorem :: XXREAL_0:27

proof end;

theorem :: XXREAL_0:28

theorem :: XXREAL_0:29

theorem :: XXREAL_0:30

proof end;

theorem :: XXREAL_0:31

proof end;

theorem :: XXREAL_0:32

for a, c, b being ext-real number st a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds

c <= d ) holds

c = max (a,b)

c <= d ) holds

c = max (a,b)

proof end;

theorem :: XXREAL_0:33

proof end;

theorem :: XXREAL_0:34

proof end;

theorem :: XXREAL_0:35

proof end;

theorem :: XXREAL_0:36

proof end;

theorem Th37: :: XXREAL_0:37

proof end;

theorem :: XXREAL_0:38

proof end;

theorem :: XXREAL_0:39

proof end;

theorem :: XXREAL_0:40

for a, b, c being ext-real number holds max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))

proof end;

theorem :: XXREAL_0:41

proof end;

theorem :: XXREAL_0:42

proof end;

theorem :: XXREAL_0:43

proof end;

theorem :: XXREAL_0:44

proof end;

begin

theorem :: XXREAL_0:45

proof end;

theorem :: XXREAL_0:46

proof end;

theorem :: XXREAL_0:47

proof end;

theorem :: XXREAL_0:48

proof end;

definition

let x, y be ext-real number ;

let a, b be set ;

func IFGT (x,y,a,b) -> set equals :Def11: :: XXREAL_0:def 11

a if x > y

otherwise b;

correctness

coherence

( ( x > y implies a is set ) & ( not x > y implies b is set ) );

consistency

for b_{1} being set holds verum;

;

end;
let a, b be set ;

func IFGT (x,y,a,b) -> set equals :Def11: :: XXREAL_0:def 11

a if x > y

otherwise b;

correctness

coherence

( ( x > y implies a is set ) & ( not x > y implies b is set ) );

consistency

for b

;

:: deftheorem Def11 defines IFGT XXREAL_0:def 11 :

for x, y being ext-real number

for a, b being set holds

( ( x > y implies IFGT (x,y,a,b) = a ) & ( not x > y implies IFGT (x,y,a,b) = b ) );

registration

let x, y be ext-real number ;

let a, b be natural number ;

cluster IFGT (x,y,a,b) -> natural ;

coherence

IFGT (x,y,a,b) is natural by Def11;

end;
let a, b be natural number ;

cluster IFGT (x,y,a,b) -> natural ;

coherence

IFGT (x,y,a,b) is natural by Def11;

theorem :: XXREAL_0:49

proof end;

theorem :: XXREAL_0:50

proof end;