let A be non empty closed_interval Subset of REAL; for a, b being Real st A = [.a,b.] holds
ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
let a, b be Real; ( A = [.a,b.] implies ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) )
assume A2:
A = [.a,b.]
; ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
defpred S1[ object ] means $1 = a;
deffunc H1( object ) -> Element of bool [:[.a,b.],NAT:] = [.a,b.] --> 0;
deffunc H2( object ) -> set = ([.a,(In ($1,REAL)).] --> 1) +* (].(In ($1,REAL)),b.] --> 0);
set B = BoundedFunctions A;
A3:
for s being object st s in [.a,b.] holds
( ( S1[s] implies H1(s) in BoundedFunctions A ) & ( not S1[s] implies H2(s) in BoundedFunctions A ) )
proof
let s be
object ;
( s in [.a,b.] implies ( ( S1[s] implies H1(s) in BoundedFunctions A ) & ( not S1[s] implies H2(s) in BoundedFunctions A ) ) )
assume A4:
s in [.a,b.]
;
( ( S1[s] implies H1(s) in BoundedFunctions A ) & ( not S1[s] implies H2(s) in BoundedFunctions A ) )
then reconsider r =
s as
Real ;
thus
(
S1[
s] implies
H1(
s)
in BoundedFunctions A )
( not S1[s] implies H2(s) in BoundedFunctions A )
H2(
s)
in BoundedFunctions A
proof
set g1 =
[.a,(In (s,REAL)).] --> 1;
set g2 =
].(In (s,REAL)),b.] --> 0;
B9:
(
a <= r &
r <= b )
by A4, XXREAL_1:1;
A10:
(
dom ([.a,(In (s,REAL)).] --> 1) = [.a,(In (s,REAL)).] &
dom (].(In (s,REAL)),b.] --> 0) = ].(In (s,REAL)),b.] )
by FUNCOP_1:13;
then A11:
(dom ([.a,(In (s,REAL)).] --> 1)) \/ (dom (].(In (s,REAL)),b.] --> 0)) = A
by A2, B9, XXREAL_1:167;
then A12:
dom (([.a,(In (s,REAL)).] --> 1) +* (].(In (s,REAL)),b.] --> 0)) = A
by FUNCT_4:def 1;
rng (([.a,(In (s,REAL)).] --> 1) +* (].(In (s,REAL)),b.] --> 0)) c= REAL
;
then reconsider f =
([.a,(In (s,REAL)).] --> 1) +* (].(In (s,REAL)),b.] --> 0) as
Function of
A,
REAL by A12, FUNCT_2:2;
reconsider r0 = 1 as
Real ;
for
c being
object st
c in (dom ([.a,(In (s,REAL)).] --> 1)) /\ (dom f) holds
|.(f . c).| <= r0
proof
let c be
object ;
( c in (dom ([.a,(In (s,REAL)).] --> 1)) /\ (dom f) implies |.(f . c).| <= r0 )
assume
c in (dom ([.a,(In (s,REAL)).] --> 1)) /\ (dom f)
;
|.(f . c).| <= r0
then A16:
c in dom ([.a,(In (s,REAL)).] --> 1)
by FUNCT_4:10, XBOOLE_1:28;
then
|.(([.a,(In (s,REAL)).] --> 1) . c).| = 1
by FUNCOP_1:7;
then
|.((f | (dom ([.a,(In (s,REAL)).] --> 1))) . c).| = 1
by FUNCT_4:33, A10, XXREAL_1:90;
hence
|.(f . c).| <= r0
by A16, FUNCT_1:49;
verum
end;
then A17:
f | (dom ([.a,(In (s,REAL)).] --> 1)) is
bounded
by RFUNCT_1:73;
reconsider s0 =
0 as
Real ;
for
c being
object st
c in (dom (].(In (s,REAL)),b.] --> 0)) /\ (dom f) holds
|.(f . c).| <= s0
proof
let c be
object ;
( c in (dom (].(In (s,REAL)),b.] --> 0)) /\ (dom f) implies |.(f . c).| <= s0 )
assume
c in (dom (].(In (s,REAL)),b.] --> 0)) /\ (dom f)
;
|.(f . c).| <= s0
then A18:
c in dom (].(In (s,REAL)),b.] --> 0)
by FUNCT_4:10, XBOOLE_1:28;
then
|.((].(In (s,REAL)),b.] --> 0) . c).| = 0
by FUNCOP_1:7;
then
|.((f | (dom (].(In (s,REAL)),b.] --> 0))) . c).| = 0
by FUNCT_4:23;
hence
|.(f . c).| <= s0
by A18, FUNCT_1:49;
verum
end;
then
f | (dom (].(In (s,REAL)),b.] --> 0)) is
bounded
by RFUNCT_1:73;
then
f | A is
bounded
by A11, A17, RFUNCT_1:87;
hence
H2(
s)
in BoundedFunctions A
;
verum
end;
hence
( not
S1[
s] implies
H2(
s)
in BoundedFunctions A )
;
verum
end;
consider x being Function of [.a,b.],(BoundedFunctions A) such that
A19:
for s being object st s in [.a,b.] holds
( ( S1[s] implies x . s = H1(s) ) & ( not S1[s] implies x . s = H2(s) ) )
from FUNCT_2:sch 5(A3);
reconsider x = x as Function of A,(BoundedFunctions A) by A2;
take
x
; for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
proof
let s be
Real;
( s in [.a,b.] implies ( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) )
assume A20:
s in [.a,b.]
;
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
In (
s,
REAL)
= s
;
hence
( (
s = a implies
x . s = [.a,b.] --> 0 ) & (
s <> a implies
x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
by A19, A20;
verum
end;
hence
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
; verum