:: by J\'ozef Bia{\l}as and Yatsuka Nakamura

::

:: Received February 16, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

theorem Th5: :: URYSOHN2:5

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 ) )

( 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 A being non empty Interval

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

x ** A is open_interval

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

x ** A is open_interval

proof end;

theorem Th8: :: URYSOHN2:8

for A being non empty Interval

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

x ** A is closed_interval

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

x ** A is closed_interval

proof end;

theorem Th9: :: URYSOHN2:9

for A being non empty Interval

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

x ** A is right_open_interval

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

x ** A is right_open_interval

proof end;

theorem Th10: :: URYSOHN2:10

for A being non empty Interval

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

x ** A is left_open_interval

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

x ** A is left_open_interval

proof end;

theorem Th11: :: URYSOHN2:11

for A being non empty Interval

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

x ** A is left_open_interval

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

x ** A is left_open_interval

proof end;

theorem Th12: :: URYSOHN2:12

for A being non empty Interval

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

x ** A is right_open_interval

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

x ** A is right_open_interval

proof end;

theorem :: URYSOHN2:13

for A being non empty Interval

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).] holds

( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).] holds

( B = [.(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

proof end;

theorem :: URYSOHN2:14

for A being non empty Interval

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds

( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).] holds

( B = ].(inf B),(sup B).] & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

proof end;

theorem :: URYSOHN2:15

for A being non empty Interval

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds

( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = ].(inf A),(sup A).[ holds

( B = ].(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

proof end;

theorem :: URYSOHN2:16

for A being non empty Interval

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds

( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

for x being Real st 0 < x holds

for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds

( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds

( inf B = x * s & sup B = x * t ) ) )

proof end;

registration

let A be interval Subset of REAL;

let x be Real;

correctness

coherence

x ** A is interval ;

end;
let x be Real;

correctness

coherence

x ** A is interval ;

proof end;

Lm1: for A being non empty Subset of REAL

for x being Real st x > 0 & x ** A is bounded_above holds

A is bounded_above

proof end;

theorem Th18: :: URYSOHN2:18

for A being non empty Subset of REAL

for x being Real

for y being R_eal st x = y & 0 <= y holds

sup (x ** A) = y * (sup A)

for x being Real

for y being R_eal st x = y & 0 <= y holds

sup (x ** A) = y * (sup A)

proof end;

Lm2: for A being non empty Subset of REAL

for x being Real st x > 0 & x ** A is bounded_below holds

A is bounded_below

proof end;

theorem Th19: :: URYSOHN2:19

for A being non empty Subset of REAL

for x being Real

for y being R_eal st x = y & 0 <= y holds

inf (x ** A) = y * (inf A)

for x being Real

for y being R_eal st x = y & 0 <= y holds

inf (x ** A) = y * (inf A)

proof end;

theorem Th24: :: URYSOHN2:24

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 )

ex c being Real st

( c in DYADIC & a < c & c < b )

proof end;

theorem :: URYSOHN2:26

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 )

for a, b being R_eal st A c= [.a,b.] holds

( a <= inf A & sup A <= b )

proof end;

theorem :: URYSOHN2:31

for eps being Real st 0 < eps holds

for d being Real st 0 < d holds

ex r1, r2 being Real st

( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )

for d being Real st 0 < d holds

ex r1, r2 being Real st

( r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps )

proof end;

:: missing, 2008.06.10, A.T.

theorem :: URYSOHN2:32

for A being non empty Subset of REAL

for x being Real st x > 0 & x ** A is bounded_above holds

A is bounded_above by Lm1;

for x being Real st x > 0 & x ** A is bounded_above holds

A is bounded_above by Lm1;

theorem :: URYSOHN2:33

for A being non empty Subset of REAL

for x being Real st x > 0 & x ** A is bounded_below holds

A is bounded_below by Lm2;

for x being Real st x > 0 & x ** A is bounded_below holds

A is bounded_below by Lm2;