:: URYSOHN2 semantic presentation

for A being Interval st A <> {} holds
( ( ^^ A <' A ^^ implies vol A = (A ^^ ) - (^^ A) ) & ( A ^^ = ^^ A implies vol A = 0. ) )

proof end;

theorem :: URYSOHN2:2

for A being Subset of REAL
for x being Real st x <> 0 holds
(x " ) * (x * A) = A

proof end;

theorem Th3: :: URYSOHN2:3

for x being Real st x <> 0 holds
for A being Subset of REAL st A = REAL holds
x * A = A

proof end;

theorem Th4: :: URYSOHN2:4

for A being Subset of REAL st A <> {} holds
0 * A = {0}

proof end;

theorem Th5: :: URYSOHN2:5

for x being Real holds x * {} = {}

proof end;

theorem Th6: :: URYSOHN2:6

for a, b being R_eal holds
( not a <=' b or ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) )

proof end;

theorem Th7: :: URYSOHN2:7

for x being R_eal holds [.x,x.] is Interval

proof end;

theorem Th8: :: URYSOHN2:8

for A being Interval holds 0 * A is Interval

proof end;

theorem Th9: :: URYSOHN2:9

for A being Interval
for x being Real st x <> 0 & A is open_interval holds
x * A is open_interval

proof end;

theorem Th10: :: URYSOHN2:10

for A being Interval
for x being Real st x <> 0 & A is closed_interval holds
x * A is closed_interval

proof end;

theorem Th11: :: URYSOHN2:11

for A being Interval
for x being Real st 0 < x & A is right_open_interval holds
x * A is right_open_interval

proof end;

theorem Th12: :: URYSOHN2:12

for A being Interval
for x being Real st x < 0 & A is right_open_interval holds
x * A is left_open_interval

proof end;

theorem Th13: :: URYSOHN2:13

for A being Interval
for x being Real st 0 < x & A is left_open_interval holds
x * A is left_open_interval

proof end;

theorem Th14: :: URYSOHN2:14

for A being Interval
for x being Real st x < 0 & A is left_open_interval holds
x * A is right_open_interval

proof end;

theorem Th15: :: URYSOHN2:15

for A being Interval st A <> {} holds
for x being Real st 0 < x holds
for B being Interval st B = x * A & A = [.(^^ A),(A ^^ ).] holds
( B = [.(^^ B),(B ^^ ).] & ( for s, t being Real st s = ^^ A & t = A ^^ holds
( ^^ B = x * s & B ^^ = x * t ) ) )

proof end;

theorem Th16: :: URYSOHN2:16

for A being Interval st A <> {} holds
for x being Real st 0 < x holds
for B being Interval st B = x * A & A = ].(^^ A),(A ^^ ).] holds
( B = ].(^^ B),(B ^^ ).] & ( for s, t being Real st s = ^^ A & t = A ^^ holds
( ^^ B = x * s & B ^^ = x * t ) ) )

proof end;

theorem Th17: :: URYSOHN2:17

for A being Interval st A <> {} holds
for x being Real st 0 < x holds
for B being Interval st B = x * A & A = ].(^^ A),(A ^^ ).[ holds
( B = ].(^^ B),(B ^^ ).[ & ( for s, t being Real st s = ^^ A & t = A ^^ holds
( ^^ B = x * s & B ^^ = x * t ) ) )

proof end;

theorem Th18: :: URYSOHN2:18

for A being Interval st A <> {} holds
for x being Real st 0 < x holds
for B being Interval st B = x * A & A = [.(^^ A),(A ^^ ).[ holds
( B = [.(^^ B),(B ^^ ).[ & ( for s, t being Real st s = ^^ A & t = A ^^ holds
( ^^ B = x * s & B ^^ = x * t ) ) )

proof end;

theorem Th19: :: URYSOHN2:19

for A being Interval
for x being Real holds x * A is Interval

proof end;

registration

let A be Interval;
let x be Real;
cluster x * A -> interval ;
correctness by Th19;

end;

theorem :: URYSOHN2:20

for A being Interval
for x being Real st 0 <= x holds
for y being Real st y = vol A holds
x * y = vol (x * A)

proof end;

theorem :: URYSOHN2:21

canceled;

theorem :: URYSOHN2:22

canceled;

theorem Th23: :: URYSOHN2:23

for eps being Real st 0 < eps holds
ex n being Nat st 1 < (2 |^ n) * eps

proof end;

theorem Th24: :: URYSOHN2:24

for a, b being Real st 0 <= a & 1 < b - a holds
ex n being Nat st
( a < n & n < b )

proof end;

theorem :: URYSOHN2:25

canceled;

theorem :: URYSOHN2:26

canceled;

theorem :: URYSOHN2:27

for n being Nat holds dyadic n c= DYADIC

proof end;

theorem Th28: :: URYSOHN2:28

for a, b being Real st a < b & 0 <= a & b <= 1 holds
ex c being Real st
( c in DYADIC & a < c & c < b )

proof end;

theorem Th29: :: URYSOHN2:29

for a, b being Real st a < b holds
ex c being Real st
( c in DOM & a < c & c < b )

proof end;

theorem :: URYSOHN2:30

for A being non empty Subset of ExtREAL
for a, b being R_eal st A c= [.a,b.] holds
( a <=' inf A & sup A <=' b )

proof end;

theorem :: URYSOHN2:31

( 0 in DYADIC & 1 in DYADIC )

proof end;

theorem :: URYSOHN2:32

for a, b being R_eal st a = 0 & b = 1 holds
DYADIC c= [.a,b.]

proof end;

theorem :: URYSOHN2:33

for n, k being Nat st n <= k holds
dyadic n c= dyadic k

proof end;

theorem Th34: :: URYSOHN2:34

for a, b, c, d being Real st a < c & c < b & a < d & d < b holds
abs (d - c) < b - a

proof end;

theorem :: URYSOHN2:35

for eps being Real st 0 < eps holds
for d being Real st 0 < d & d <= 1 holds
ex r1, r2 being Real st
( r1 in DYADIC \/ R>1 & r2 in DYADIC \/ R>1 & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )

proof end;