scheme
RealContinuity{
P1[
object ],
P2[
object ] } :
ex
z being
Real st
for
x,
y being
Real st
P1[
x] &
P2[
y] holds
(
x <= z &
z <= y )
provided
A1:
for
x,
y being
Real st
P1[
x] &
P2[
y] holds
x <= y
theorem Th14:
for
a being
Real st 1
< a holds
a < a ^2
Lm1:
for a being Real st 0 < a holds
ex x being Real st
( 0 < x & x ^2 < a )
Lm2:
for x, y being Real st 0 <= x & 0 <= y & x ^2 = y ^2 holds
x = y
Lm3:
for x, y being Real st 0 <= x & x < y holds
sqrt x < sqrt y
Lm4:
2 ^2 = 2 * 2
;
Lm5:
for a, b being Real st 0 <= a & 0 <= b & a <> b holds
((sqrt a) ^2) - ((sqrt b) ^2) <> 0
theorem
for
a being
Real st
a ^2 < 1 holds
(
- 1
< a &
a < 1 )
Lm6:
for a, b being Real st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(1 + (a ^2)) * (b ^2) <= 1 + (b ^2)
Lm7:
for a, b being Real st b <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
Lm8:
for a, b being Real st a <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
Lm9:
for a, b being Real st a >= 0 & a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
:: let x,y be real number;
:: cluster min(x,y) -> real;
:: coherence by XREAL_0:def 1;
:: cluster max(x,y) -> real;
:: coherence by XREAL_0:def 1;
:: end;