:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
registration
let
T
be non
empty
TopSpace
;
let
f
,
g
be
continuous
RealMap
of
T
;
set
c
= the
carrier
of
T
;
reconsider
F
=
f
,
G
=
g
as
continuous
Function
of
T
,
R^1
by
JORDAN5A:27
,
TOPMETR:17
;
cluster
f
+
g
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
f
+
g
holds
b
1
is
continuous
proof
end;
cluster
f
-
g
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
f
-
g
holds
b
1
is
continuous
proof
end;
cluster
f
(#)
g
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
f
(#)
g
holds
b
1
is
continuous
proof
end;
end;
registration
let
T
be non
empty
TopSpace
;
let
f
be
continuous
RealMap
of
T
;
cluster
-
f
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
-
f
holds
b
1
is
continuous
proof
end;
end;
registration
let
T
be non
empty
TopSpace
;
let
f
be
continuous
RealMap
of
T
;
cluster
|.
f
.|
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
abs
f
holds
b
1
is
continuous
proof
end;
end;
Lm1
:
now
:: thesis:
for
T
being non
empty
TopSpace
for
a
being
Element
of
REAL
holds the
carrier
of
T
-->
a
is
continuous
let
T
be non
empty
TopSpace
;
:: thesis:
for
a
being
Element
of
REAL
holds the
carrier
of
T
-->
a
is
continuous
let
a
be
Element
of
REAL
;
:: thesis:
the
carrier
of
T
-->
a
is
continuous
set
c
= the
carrier
of
T
;
set
f
= the
carrier
of
T
-->
a
;
thus
the
carrier
of
T
-->
a
is
continuous
:: thesis:
verum
proof
let
Y
be
Subset
of
REAL
;
:: according to
PSCOMP_1:def 3
:: thesis:
( not
Y
is
closed
or
(
the
carrier
of
T
-->
a
)
"
Y
is
closed
)
A1
:
dom
(
the
carrier
of
T
-->
a
)
=
the
carrier
of
T
by
FUNCT_2:def 1
;
assume
Y
is
closed
;
:: thesis:
(
the
carrier
of
T
-->
a
)
"
Y
is
closed
A2
:
rng
(
the
carrier
of
T
-->
a
)
=
{
a
}
by
FUNCOP_1:8
;
per
cases
(
a
in
Y
or not
a
in
Y
)
;
suppose
a
in
Y
;
:: thesis:
(
the
carrier
of
T
-->
a
)
"
Y
is
closed
then
A3
:
rng
(
the
carrier
of
T
-->
a
)
c=
Y
by
A2
,
ZFMISC_1:31
;
(
the
carrier
of
T
-->
a
)
"
Y
=
(
the
carrier
of
T
-->
a
)
"
(
(
rng
(
the
carrier
of
T
-->
a
)
)
/\
Y
)
by
RELAT_1:133
.=
(
the
carrier
of
T
-->
a
)
"
(
rng
(
the
carrier
of
T
-->
a
)
)
by
A3
,
XBOOLE_1:28
.= the
carrier
of
T
by
A1
,
RELAT_1:134
.=
[#]
T
;
hence
(
the
carrier
of
T
-->
a
)
"
Y
is
closed
;
:: thesis:
verum
end;
suppose
not
a
in
Y
;
:: thesis:
(
the
carrier
of
T
-->
a
)
"
Y
is
closed
then
A4
:
rng
(
the
carrier
of
T
-->
a
)
misses
Y
by
A2
,
ZFMISC_1:50
;
(
the
carrier
of
T
-->
a
)
"
Y
=
(
the
carrier
of
T
-->
a
)
"
(
(
rng
(
the
carrier
of
T
-->
a
)
)
/\
Y
)
by
RELAT_1:133
.=
(
the
carrier
of
T
-->
a
)
"
{}
by
A4
,
XBOOLE_0:def 7
.=
{}
T
;
hence
(
the
carrier
of
T
-->
a
)
"
Y
is
closed
;
:: thesis:
verum
end;
end;
end;
end;
reconsider
jj
= 1 as
Element
of
REAL
by
XREAL_0:def 1
;
registration
let
T
be non
empty
TopSpace
;
cluster
V1
()
V4
( the
carrier
of
T
)
V5
(
REAL
) non
empty
Function-like
V32
( the
carrier
of
T
)
V36
( the
carrier
of
T
,
REAL
)
V145
()
V146
()
V147
()
continuous
positive-yielding
for
Element
of
K16
(
K17
( the
carrier
of
T
,
REAL
));
existence
ex
b
1
being
RealMap
of
T
st
(
b
1
is
positive-yielding
&
b
1
is
continuous
)
proof
end;
cluster
V1
()
V4
( the
carrier
of
T
)
V5
(
REAL
) non
empty
Function-like
V32
( the
carrier
of
T
)
V36
( the
carrier
of
T
,
REAL
)
V145
()
V146
()
V147
()
continuous
negative-yielding
for
Element
of
K16
(
K17
( the
carrier
of
T
,
REAL
));
existence
ex
b
1
being
RealMap
of
T
st
(
b
1
is
negative-yielding
&
b
1
is
continuous
)
proof
end;
end;
registration
let
T
be non
empty
TopSpace
;
let
f
be
continuous
nonnegative-yielding
RealMap
of
T
;
cluster
sqrt
f
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
sqrt
f
holds
b
1
is
continuous
proof
end;
end;
registration
let
T
be non
empty
TopSpace
;
let
f
be
continuous
RealMap
of
T
;
let
r
be
Real
;
cluster
r
(#)
f
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
r
(#)
f
holds
b
1
is
continuous
proof
end;
end;
registration
let
T
be non
empty
TopSpace
;
let
f
be
non-empty
continuous
RealMap
of
T
;
cluster
K487
(
f
)
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
f
^
holds
b
1
is
continuous
proof
end;
end;
registration
let
T
be non
empty
TopSpace
;
let
f
be
continuous
RealMap
of
T
;
let
g
be
non-empty
continuous
RealMap
of
T
;
cluster
K484
(
f
,
g
)
->
continuous
for
RealMap
of
T
;
coherence
for
b
1
being
RealMap
of
T
st
b
1
=
f
/
g
holds
b
1
is
continuous
proof
end;
end;