let n be Nat; :: thesis: for TM being metrizable TopSpace
for A, B being Subset of TM st A is closed & B is closed & A misses B holds
for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds
ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 )
let TM be metrizable TopSpace; :: thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds
for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds
ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 )
let A, B be Subset of TM; :: thesis: ( A is closed & B is closed & A misses B implies for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds
ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 ) )
assume that
A1: ( A is closed & B is closed ) and
A2: A misses B ; :: thesis: for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds
ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 )
let H be Subset of TM; :: thesis: ( ind H <= n & TM | H is second-countable & TM | H is finite-ind implies ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 ) )
assume that
A3: ind H <= n and
A4: ( TM | H is second-countable & TM | H is finite-ind ) ; :: thesis: ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 )
H is finite-ind by A4, TOPDIM_1:18;
then ind H = ind (TM | H) by TOPDIM_1:17;
then consider a, b being Subset of (TM | H) such that
A5: [#] (TM | H) = a \/ b and
a misses b and
A6: ind a <= n - 1 and
A7: ind b <= 0 by A3, A4, Lm3;
[#] (TM | H) c= [#] TM by PRE_TOPC:def 4;
then reconsider aa = a, bb = b as Subset of TM by XBOOLE_1:1;
A8: bb is finite-ind by A4, TOPDIM_1:22;
A9: H = aa \/ bb by A5, PRE_TOPC:def 5;
then A10: bb /\ H = bb by XBOOLE_1:7, XBOOLE_1:28;
( ind b = ind bb & (TM | H) | b = TM | bb ) by A4, METRIZTS:9, TOPDIM_1:22;
then consider L being Subset of TM such that
A11: L separates A,B and
A12: L misses bb by A1, A2, A4, A7, A8, TOPDIM_1:37;
take L ; :: thesis: ( L separates A,B & ind (L /\ H) <= n - 1 )
( L /\ H misses bb & L /\ H c= H ) by A10, A12, XBOOLE_1:17, XBOOLE_1:76;
then ( aa is finite-ind & L /\ H c= aa ) by A4, A9, TOPDIM_1:22, XBOOLE_1:73;
then ( ind a = ind aa & ind (L /\ H) <= ind aa ) by TOPDIM_1:19, TOPDIM_1:21;
hence ( L separates A,B & ind (L /\ H) <= n - 1 ) by A6, A11, XXREAL_0:2; :: thesis: verum