let M be non empty MetrSpace; for F, G being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds
L is Lebesgue_number of G
let F, G be open Subset-Family of (TopSpaceMetr M); for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds
L is Lebesgue_number of G
let L be Lebesgue_number of F; ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G implies L is Lebesgue_number of G )
assume that
A1:
TopSpaceMetr M is compact
and
A2:
F is Cover of (TopSpaceMetr M)
and
A3:
F is_finer_than G
; L is Lebesgue_number of G
set TM = TopSpaceMetr M;
A4:
now for x being Point of M ex B being Subset of (TopSpaceMetr M) st
( B in G & Ball (x,L) c= B )let x be
Point of
M;
ex B being Subset of (TopSpaceMetr M) st
( B in G & Ball (x,L) c= B )consider A being
Subset of
(TopSpaceMetr M) such that A5:
A in F
and A6:
Ball (
x,
L)
c= A
by A1, A2, Def1;
consider B being
set such that A7:
B in G
and A8:
A c= B
by A3, A5, SETFAM_1:def 2;
reconsider B =
B as
Subset of
(TopSpaceMetr M) by A7;
take B =
B;
( B in G & Ball (x,L) c= B )thus
(
B in G &
Ball (
x,
L)
c= B )
by A6, A7, A8;
verum end;
( union F = [#] (TopSpaceMetr M) & union F c= union G )
by A2, A3, SETFAM_1:13, SETFAM_1:45;
then
G is Cover of (TopSpaceMetr M)
by SETFAM_1:def 11;
hence
L is Lebesgue_number of G
by A1, A4, Def1; verum