begin
:: deftheorem Def1 defines ext-real XXREAL_0:def 1 :
:: deftheorem defines +infty XXREAL_0:def 2 :
:: deftheorem defines -infty XXREAL_0:def 3 :
:: deftheorem defines ExtREAL XXREAL_0:def 4 :
definition
let x,
y be
ext-real number ;
pred x <= y means :
Def5:
ex
x',
y' being
Element of
REAL+ st
(
x = x' &
y = y' &
x' <=' y' )
if (
x in REAL+ &
y in REAL+ )
ex
x',
y' being
Element of
REAL+ st
(
x = [0 ,x'] &
y = [0 ,y'] &
y' <=' x' )
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 x', y' being Element of REAL+ st
( x = x' & y = y' & x' <=' y' ) iff ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & y' <=' x' ) ) )
by ARYTM_0:5, XBOOLE_0:3;
reflexivity
for x being ext-real number holds
( ( x in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & x = y' & x' <=' y' ) ) & ( x in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( x = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( 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 ) )
connectedness
for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) or ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not y = [0 ,y'] or not y' <=' x' ) ) ) 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 x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( 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;
:: 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
x',
y' being
Element of
REAL+ st
(
x = x' &
y = y' &
x' <=' y' ) ) ) & (
x in [:{0 },REAL+ :] &
y in [:{0 },REAL+ :] implies (
x <= y iff ex
x',
y' being
Element of
REAL+ st
(
x = [0 ,x'] &
y = [0 ,y'] &
y' <=' x' ) ) ) & ( ( 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 ) ) ) );
Lm1:
+infty <> [0 ,0 ]
Lm2:
not +infty in REAL+
by ARYTM_0:1, ORDINAL1:7;
Lm3:
not -infty in REAL+
Lm4:
not +infty in [:{0 },REAL+ :]
Lm5:
not -infty in [:{0 },REAL+ :]
Lm6:
-infty < +infty
theorem Th1:
Lm7:
for a being ext-real number st -infty >= a holds
a = -infty
Lm8:
for a being ext-real number st +infty <= a holds
a = +infty
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
Lm9:
for a being ext-real number holds
( a in REAL or a = +infty or a = -infty )
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
begin
:: deftheorem defines positive XXREAL_0:def 6 :
:: deftheorem defines negative XXREAL_0:def 7 :
:: deftheorem defines zero XXREAL_0:def 8 :
begin
:: deftheorem Def9 defines min XXREAL_0:def 9 :
:: deftheorem Def10 defines max XXREAL_0:def 10 :
theorem
theorem
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th25:
theorem Th26:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th37:
theorem
theorem
theorem
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)
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
:: deftheorem Def11 defines IFGT XXREAL_0:def 11 :
theorem
theorem