let n be Nat; for TM being metrizable TopSpace
for H being Subset of TM st TM | H is second-countable holds
( ( H is finite-ind & ind H <= n ) iff for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )
let TM be metrizable TopSpace; for H being Subset of TM st TM | H is second-countable holds
( ( H is finite-ind & ind H <= n ) iff for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )
let M be Subset of TM; ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )
assume A1:
TM | M is second-countable
; ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )
hereby ( ( for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) implies ( M is finite-ind & ind M <= n ) )
assume that A2:
M is
finite-ind
and A3:
ind M <= n
;
for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )let p be
Point of
TM;
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )let U be
open Subset of
TM;
( p in U implies ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )assume A4:
p in U
;
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )reconsider P =
{p} as
Subset of
TM by A4, ZFMISC_1:31;
( not
TM is
empty & not
p in U ` )
by A4, XBOOLE_0:def 5;
then consider L being
Subset of
TM such that A5:
L separates P,
U `
and A6:
ind (L /\ M) <= n - 1
by A1, A2, A3, Th11, ZFMISC_1:50;
consider W,
W1 being
open Subset of
TM such that A7:
P c= W
and A8:
U ` c= W1
and A9:
W misses W1
and A10:
L = (W \/ W1) `
by A5, METRIZTS:def 3;
take W =
W;
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )
(
W c= W1 ` &
W1 ` c= (U `) ` )
by A8, A9, SUBSET_1:12, SUBSET_1:23;
hence
(
p in W &
W c= U )
by A7, ZFMISC_1:31;
( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )
Cl W misses W1
by A9, TSEP_1:36;
then
(Cl W) \ W1 = Cl W
by XBOOLE_1:83;
then Fr W =
((Cl W) \ W1) \ W
by TOPS_1:42
.=
(Cl W) \ (W \/ W1)
by XBOOLE_1:41
.=
(Cl W) /\ L
by A10, SUBSET_1:13
;
then
Fr W c= L
by XBOOLE_1:17;
then A11:
M /\ (Fr W) c= M /\ L
by XBOOLE_1:27;
M /\ L c= M
by XBOOLE_1:17;
then A12:
M /\ L is
finite-ind
by A2, TOPDIM_1:19;
then
ind (M /\ (Fr W)) <= ind (M /\ L)
by A11, TOPDIM_1:19;
hence
(
M /\ (Fr W) is
finite-ind &
ind (M /\ (Fr W)) <= n - 1 )
by A6, A11, A12, TOPDIM_1:19, XXREAL_0:2;
verum
end;
set Tm = TM | M;
assume A13:
for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )
; ( M is finite-ind & ind M <= n )
A14:
for p being Point of (TM | M)
for U being open Subset of (TM | M) st p in U holds
ex W being open Subset of (TM | M) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
proof
A15:
[#] (TM | M) = M
by PRE_TOPC:def 5;
let p be
Point of
(TM | M);
for U being open Subset of (TM | M) st p in U holds
ex W being open Subset of (TM | M) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )let U be
open Subset of
(TM | M);
( p in U implies ex W being open Subset of (TM | M) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
assume A16:
p in U
;
ex W being open Subset of (TM | M) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
p in M
by A15, A16;
then reconsider p9 =
p as
Point of
TM ;
consider U9 being
Subset of
TM such that A17:
U9 is
open
and A18:
U = U9 /\ the
carrier of
(TM | M)
by TSP_1:def 1;
p9 in U9
by A16, A18, XBOOLE_0:def 4;
then consider W9 being
open Subset of
TM such that A19:
(
p9 in W9 &
W9 c= U9 )
and A20:
M /\ (Fr W9) is
finite-ind
and A21:
ind (M /\ (Fr W9)) <= n - 1
by A13, A17;
reconsider W =
W9 /\ the
carrier of
(TM | M) as
Subset of
(TM | M) by XBOOLE_1:17;
reconsider W =
W as
open Subset of
(TM | M) by TSP_1:def 1;
take
W
;
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
thus
(
p in W &
W c= U )
by A16, A18, A19, XBOOLE_0:def 4, XBOOLE_1:26;
( Fr W is finite-ind & ind (Fr W) <= n - 1 )
reconsider FrW =
Fr W as
Subset of
TM by A15, XBOOLE_1:1;
A22:
FrW c= (Fr W9) /\ M
by A15, TOPDIM_1:1;
then A23:
FrW is
finite-ind
by A20, TOPDIM_1:19;
ind FrW <= ind ((Fr W9) /\ M)
by A20, A22, TOPDIM_1:19;
then
ind (Fr W) <= ind ((Fr W9) /\ M)
by A23, TOPDIM_1:21;
hence
(
Fr W is
finite-ind &
ind (Fr W) <= n - 1 )
by A21, A23, TOPDIM_1:21, XXREAL_0:2;
verum
end;
then A24:
TM | M is finite-ind
by TOPDIM_1:15;
then A25:
M is finite-ind
by TOPDIM_1:18;
ind (TM | M) <= n
by A14, A24, TOPDIM_1:16;
hence
( M is finite-ind & ind M <= n )
by A25, TOPDIM_1:17; verum