:: Introduction to Arithmetic of Extended Real Numbers
:: by Library Committee
::
:: Received January 4, 2006
:: Copyright (c) 2006 Association of Mizar Users
:: 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:
:: XXREAL_0:def 5
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: :: XXREAL_0:1
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: :: XXREAL_0:2
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 )
theorem Th9: :: XXREAL_0:9
theorem Th10: :: XXREAL_0:10
theorem Th11: :: XXREAL_0:11
theorem Th12: :: XXREAL_0:12
theorem Th13: :: XXREAL_0:13
theorem :: XXREAL_0:14
:: deftheorem defines positive XXREAL_0:def 6 :
:: deftheorem defines negative XXREAL_0:def 7 :
:: deftheorem defines zero XXREAL_0:def 8 :
:: deftheorem Def9 defines min XXREAL_0:def 9 :
:: deftheorem Def10 defines max XXREAL_0:def 10 :
theorem :: XXREAL_0:15
theorem :: XXREAL_0:16
theorem Th17: :: XXREAL_0:17
theorem Th18: :: XXREAL_0:18
theorem :: XXREAL_0:19
theorem :: XXREAL_0:20
theorem :: XXREAL_0:21
theorem :: XXREAL_0:22
theorem :: XXREAL_0:23
theorem :: XXREAL_0:24
theorem Th25: :: XXREAL_0:25
theorem Th26: :: XXREAL_0:26
theorem :: XXREAL_0:27
theorem :: XXREAL_0:28
theorem :: XXREAL_0:29
theorem :: XXREAL_0:30
theorem :: XXREAL_0:31
theorem :: XXREAL_0:32
theorem :: XXREAL_0:33
theorem :: XXREAL_0:34
theorem :: XXREAL_0:35
theorem :: XXREAL_0:36
theorem Th37: :: XXREAL_0:37
theorem :: XXREAL_0:38
theorem :: XXREAL_0:39
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)
theorem :: XXREAL_0:41
theorem :: XXREAL_0:42
theorem :: XXREAL_0:43
theorem :: XXREAL_0:44
theorem :: XXREAL_0:45
theorem :: XXREAL_0:46
theorem :: XXREAL_0:47
theorem :: XXREAL_0:48
:: deftheorem Def11 defines IFGT XXREAL_0:def 11 :
theorem :: XXREAL_0:49
theorem :: XXREAL_0:50