:: URYSOHN2 semantic presentation
begin
theorem
:: URYSOHN2:1
for
A
being ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<>
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
(
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
"
)
: ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) )
**
(
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: URYSOHN2:2
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<>
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
for
A
being ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
=
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: URYSOHN2:3
for
A
being ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
<>
{}
: ( ( ) (
empty
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
)
set
) holds
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
**
A
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: URYSOHN2:4
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
{}
: ( ( ) (
empty
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
)
set
) : ( ( ) (
empty
proper
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
open_interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
)
set
) ;
theorem
:: URYSOHN2:5
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) holds
( not
a
: ( ( ) (
ext-real
)
R_eal
)
<=
b
: ( ( ) (
ext-real
)
R_eal
) or (
a
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) ( non
empty
non
real
ext-real
non
positive
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
b
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) ( non
empty
non
real
ext-real
non
positive
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) or (
a
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) ( non
empty
non
real
ext-real
non
positive
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
b
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) or (
a
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) ( non
empty
non
real
ext-real
non
positive
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
b
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) ( non
empty
non
real
ext-real
positive
non
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) or (
a
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) &
b
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) or (
a
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) &
b
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) ( non
empty
non
real
ext-real
positive
non
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) or (
a
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) ( non
empty
non
real
ext-real
positive
non
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
b
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) ( non
empty
non
real
ext-real
positive
non
negative
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ) ) ;
theorem
:: URYSOHN2:6
for
A
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) holds
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
**
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
interval
;
theorem
:: URYSOHN2:7
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<>
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) is
open_interval
holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
open_interval
;
theorem
:: URYSOHN2:8
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<>
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) is
closed_interval
holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
closed_interval
;
theorem
:: URYSOHN2:9
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) is
right_open_interval
holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
right_open_interval
;
theorem
:: URYSOHN2:10
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) is
right_open_interval
holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
left_open_interval
;
theorem
:: URYSOHN2:11
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) is
left_open_interval
holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
left_open_interval
;
theorem
:: URYSOHN2:12
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) is
left_open_interval
holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
right_open_interval
;
theorem
:: URYSOHN2:13
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
for
B
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) st
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
(
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.]
: ( ( ) (
ext-real-membered
interval
)
set
) holds
(
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.]
: ( ( ) (
ext-real-membered
interval
)
set
) & ( for
s
,
t
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
s
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
t
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) holds
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
s
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) &
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
t
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) ) ) ) ;
theorem
:: URYSOHN2:14
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
for
B
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) st
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
].
(
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.]
: ( ( ) (
ext-real-membered
non
left_end
interval
)
set
) holds
(
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
].
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.]
: ( ( ) (
ext-real-membered
non
left_end
interval
)
set
) & ( for
s
,
t
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
s
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
t
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) holds
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
s
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) &
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
t
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) ) ) ) ;
theorem
:: URYSOHN2:15
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
for
B
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) st
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
].
(
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
non
right_end
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
(
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
].
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.[
: ( ( ) (
complex-membered
ext-real-membered
real-membered
non
left_end
non
right_end
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) & ( for
s
,
t
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
s
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
t
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) holds
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
s
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) &
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
t
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) ) ) ) ;
theorem
:: URYSOHN2:16
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
for
B
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) st
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
(
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.[
: ( ( ) (
ext-real-membered
non
right_end
interval
)
set
) holds
(
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
=
[.
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ,
(
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
.[
: ( ( ) (
ext-real-membered
non
right_end
interval
)
set
) & ( for
s
,
t
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
s
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
inf
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
t
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
sup
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) holds
(
inf
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
s
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) &
sup
B
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
t
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) ) ) ) ;
theorem
:: URYSOHN2:17
for
A
being ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
interval
) ( non
empty
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) ;
registration
let
A
be ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
let
x
be ( ( ) (
V24
()
real
ext-real
)
Real
) ;
cluster
x
: ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) )
**
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
set
)
->
interval
;
end;
theorem
:: URYSOHN2:18
for
A
being ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
)
for
y
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
y
: ( ( ) (
ext-real
)
R_eal
) &
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<=
y
: ( ( ) (
ext-real
)
R_eal
) holds
sup
(
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
y
: ( ( ) (
ext-real
)
R_eal
)
*
(
sup
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ;
theorem
:: URYSOHN2:19
for
A
being ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
)
for
y
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
y
: ( ( ) (
ext-real
)
R_eal
) &
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<=
y
: ( ( ) (
ext-real
)
R_eal
) holds
inf
(
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
=
y
: ( ( ) (
ext-real
)
R_eal
)
*
(
inf
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ;
theorem
:: URYSOHN2:20
for
A
being ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<=
x
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
for
y
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
y
: ( ( ) (
V24
()
real
ext-real
)
Real
)
=
diameter
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) holds
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
*
y
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) )
=
diameter
(
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( (
interval
) (
complex-membered
ext-real-membered
real-membered
interval
)
Interval
)
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
interval
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) ;
theorem
:: URYSOHN2:21
for
eps
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
eps
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
ex
n
being ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) st 1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
(
2 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
|^
n
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*
eps
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) ;
theorem
:: URYSOHN2:22
for
a
,
b
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<=
a
: ( ( ) (
V24
()
real
ext-real
)
Real
) & 1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
)
-
a
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) holds
ex
n
being ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) st
(
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
n
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
n
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) ) ;
theorem
:: URYSOHN2:23
for
n
being ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
dyadic
n
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: URYSOHN2:24
for
a
,
b
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<=
a
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
b
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<=
1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
c
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
(
c
: ( ( ) (
V24
()
real
ext-real
)
Real
)
in
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
c
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
c
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) ) ;
theorem
:: URYSOHN2:25
for
a
,
b
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
ex
c
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
(
c
: ( ( ) (
V24
()
real
ext-real
)
Real
)
in
DOM
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
c
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
c
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) ) ;
theorem
:: URYSOHN2:26
for
A
being ( ( non
empty
) ( non
empty
ext-real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
a
,
b
being ( ( ) (
ext-real
)
R_eal
) st
A
: ( ( non
empty
) ( non
empty
ext-real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
[.
a
: ( ( ) (
ext-real
)
R_eal
) ,
b
: ( ( ) (
ext-real
)
R_eal
)
.]
: ( ( ) (
ext-real-membered
interval
)
set
) holds
(
a
: ( ( ) (
ext-real
)
R_eal
)
<=
inf
A
: ( ( non
empty
) ( non
empty
ext-real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) ) &
sup
A
: ( ( non
empty
) ( non
empty
ext-real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
)
Element
of
ExtREAL
: ( ( ) ( non
empty
ext-real-membered
interval
)
set
) )
<=
b
: ( ( ) (
ext-real
)
R_eal
) ) ;
theorem
:: URYSOHN2:27
(
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
in
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) & 1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
in
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: URYSOHN2:28
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
[.
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
.]
: ( ( ) (
complex-membered
ext-real-membered
real-membered
interval
)
set
) ;
theorem
:: URYSOHN2:29
for
n
,
k
being ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) st
n
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<=
k
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
dyadic
n
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
dyadic
k
: ( ( ) (
ordinal
natural
V24
()
real
ext-real
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: URYSOHN2:30
for
a
,
b
,
c
,
d
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
c
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
c
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
a
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
d
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
d
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
abs
(
d
: ( ( ) (
V24
()
real
ext-real
)
Real
)
-
c
: ( ( ) (
V24
()
real
ext-real
)
Real
)
)
: ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) )
<
b
: ( ( ) (
V24
()
real
ext-real
)
Real
)
-
a
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) ;
theorem
:: URYSOHN2:31
for
eps
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
eps
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
for
d
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
d
: ( ( ) (
V24
()
real
ext-real
)
Real
) holds
ex
r1
,
r2
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
(
r1
: ( ( ) (
V24
()
real
ext-real
)
Real
)
in
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
(
right_open_halfline
1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
r2
: ( ( ) (
V24
()
real
ext-real
)
Real
)
in
DYADIC
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
(
right_open_halfline
1 : ( ( ) ( non
empty
ordinal
natural
V24
()
real
ext-real
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
left_end
bounded_below
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
r1
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
r1
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
d
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
d
: ( ( ) (
V24
()
real
ext-real
)
Real
)
<
r2
: ( ( ) (
V24
()
real
ext-real
)
Real
) &
r2
: ( ( ) (
V24
()
real
ext-real
)
Real
)
-
r1
: ( ( ) (
V24
()
real
ext-real
)
Real
) : ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) )
<
eps
: ( ( ) (
V24
()
real
ext-real
)
Real
) ) ;
begin
theorem
:: URYSOHN2:32
for
A
being ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
bounded_above
holds
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
bounded_above
;
theorem
:: URYSOHN2:33
for
A
being ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) (
V24
()
real
ext-real
)
Real
) st
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
>
0
: ( ( ) (
empty
ordinal
natural
V24
()
real
ext-real
non
positive
non
negative
integer
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
interval
V134
() )
Element
of
NAT
: ( ( ) (
V33
()
complex-membered
ext-real-membered
real-membered
rational-membered
integer-membered
natural-membered
V72
()
bounded_below
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) &
x
: ( ( ) (
V24
()
real
ext-real
)
Real
)
**
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Element
of
K32
(
REAL
: ( ( ) ( non
empty
V33
()
V36
()
complex-membered
ext-real-membered
real-membered
V72
() non
bounded_below
non
bounded_above
interval
)
set
) ) : ( ( ) ( non
empty
)
set
) ) is
bounded_below
holds
A
: ( ( non
empty
) ( non
empty
complex-membered
ext-real-membered
real-membered
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
bounded_below
;