let r, s be Real; for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is Cover of (Closed-Interval-TSpace (r,s))
let jauge be Function of [.r,s.],].0,+infty.[; for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is Cover of (Closed-Interval-TSpace (r,s))
let S be Subset-Family of (Closed-Interval-TSpace (r,s)); ( r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } implies S is Cover of (Closed-Interval-TSpace (r,s)) )
assume that
A1:
r <= s
and
A2:
S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum }
; S is Cover of (Closed-Interval-TSpace (r,s))
[.r,s.] c= union S
proof
let x be
object ;
TARSKI:def 3 ( not x in [.r,s.] or x in union S )
assume A3:
x in [.r,s.]
;
x in union S
then reconsider x0 =
x as
Element of
[.r,s.] ;
x0 in dom jauge
by A3, PARTFUN1:def 2;
then
jauge . x0 in rng jauge
by FUNCT_1:3;
then
0 < jauge . x0
by XXREAL_1:4;
then
(
x0 - (jauge . x0) < x0 - 0 &
x0 + 0 < x0 + (jauge . x0) )
by XREAL_1:15, XREAL_1:8;
then
x0 in ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[
by XXREAL_1:4;
then A5:
x0 in ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.]
by A3, XBOOLE_0:def 4;
].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.] in S
by A2;
hence
x in union S
by A5, TARSKI:def 4;
verum
end;
then
S is Cover of [.r,s.]
by SETFAM_1:def 11;
hence
S is Cover of (Closed-Interval-TSpace (r,s))
by A1, TOPMETR:18; verum