:: TOPDIM_2 semantic presentation
begin
definition
let X be set ;
let Fx be Subset-Family of X;
attrFx is finite-order means :Def1: :: TOPDIM_2:def 1
ex n being Nat st
for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds
meet Gx is empty ;
end;
:: deftheorem Def1 defines finite-order TOPDIM_2:def_1_:_
for X being set
for Fx being Subset-Family of X holds
( Fx is finite-order iff ex n being Nat st
for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds
meet Gx is empty );
registration
let X be set ;
cluster finite-order for Element of bool (bool X);
existence
ex b1 being Subset-Family of X st b1 is finite-order
proof
reconsider E = {} as Subset-Family of X by XBOOLE_1:2;
take E ; ::_thesis: E is finite-order
take 0 ; :: according to TOPDIM_2:def_1 ::_thesis: for Gx being Subset-Family of X st Gx c= E & 0 in card Gx holds
meet Gx is empty
let G be Subset-Family of X; ::_thesis: ( G c= E & 0 in card G implies meet G is empty )
thus ( G c= E & 0 in card G implies meet G is empty ) ; ::_thesis: verum
end;
cluster finite -> finite-order for Element of bool (bool X);
coherence
for b1 being Subset-Family of X st b1 is finite holds
b1 is finite-order
proof
let F be Subset-Family of X; ::_thesis: ( F is finite implies F is finite-order )
assume F is finite ; ::_thesis: F is finite-order
then reconsider f = F as finite Subset-Family of X ;
take n = card f; :: according to TOPDIM_2:def_1 ::_thesis: for Gx being Subset-Family of X st Gx c= F & n in card Gx holds
meet Gx is empty
let G be Subset-Family of X; ::_thesis: ( G c= F & n in card G implies meet G is empty )
assume that
A1: G c= F and
A2: n in card G ; ::_thesis: meet G is empty
card G c= card F by A1, CARD_1:11;
hence meet G is empty by A2, NAT_1:44; ::_thesis: verum
end;
end;
definition
let X be set ;
let Fx be Subset-Family of X;
func order Fx -> ext-real number means :Def2: :: TOPDIM_2:def 2
( ( for Gx being Subset-Family of X st it + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = it + 1 & ( not meet Gx is empty or Gx is empty ) ) ) if Fx is finite-order
otherwise it = +infty ;
existence
( ( Fx is finite-order implies ex b1 being ext-real number st
( ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b1 being ext-real number st b1 = +infty ) )
proof
defpred S1[ Nat] means for Gx being Subset-Family of X st Gx c= Fx & $1 in card Gx holds
meet Gx is empty ;
now__::_thesis:_(_Fx_is_finite-order_implies_ex_O_being_set_st_
(_(_for_Gx_being_Subset-Family_of_X_st_O_+_1_in_card_Gx_&_Gx_c=_Fx_holds_
meet_Gx_is_empty_)_&_ex_Gx_being_Subset-Family_of_X_st_
(_Gx_c=_Fx_&_card_Gx_=_O_+_1_&_(_not_meet_Gx_is_empty_or_Gx_is_empty_)_)_)_)
assume Fx is finite-order ; ::_thesis: ex O being set st
( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) )
then A1: ex n being Nat st S1[n] by Def1;
consider k being Nat such that
A2: S1[k] and
A3: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A1);
take O = k - 1; ::_thesis: ( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) )
thus for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds
meet Gx is empty by A2; ::_thesis: ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )
thus ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) ::_thesis: verum
proof
percases ( k = 0 or k > 0 ) ;
supposeA4: k = 0 ; ::_thesis: ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )
reconsider E = {} as Subset-Family of X by XBOOLE_1:2;
take E ; ::_thesis: ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) )
thus ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) ) by A4, XBOOLE_1:2; ::_thesis: verum
end;
suppose k > 0 ; ::_thesis: ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
assume A5: for Gx being Subset-Family of X st Gx c= Fx & card Gx = O + 1 holds
( meet Gx is empty & not Gx is empty ) ; ::_thesis: contradiction
S1[k1]
proof
A6: card (card (k1 + 1)) = card (k1 + 1) ;
then A7: card (k1 + 1) = k by CARD_1:40;
let Gx be Subset-Family of X; ::_thesis: ( Gx c= Fx & k1 in card Gx implies meet Gx is empty )
assume that
A8: Gx c= Fx and
A9: k1 in card Gx ; ::_thesis: meet Gx is empty
card (card k1) = card k1 ;
then card k1 = k1 by CARD_1:40;
then nextcard k1 = card k by A6, NAT_1:42;
then card k c= card Gx by A9, CARD_3:90;
then consider f being Function such that
A10: ( f is one-to-one & dom f = k ) and
A11: rng f c= Gx by CARD_1:10;
reconsider R = rng f as Subset-Family of X by A11, XBOOLE_1:1;
k,R are_equipotent by A10, WELLORD2:def_4;
then A12: k = card R by A7, CARD_1:5;
then A13: not R is empty by A6;
R c= Fx by A8, A11, XBOOLE_1:1;
then meet R is empty by A5, A12;
then meet Gx c= {} by A11, A13, SETFAM_1:6;
hence meet Gx is empty ; ::_thesis: verum
end;
then k1 + 1 <= k1 by A3;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
end;
hence ( ( Fx is finite-order implies ex b1 being ext-real number st
( ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b1 being ext-real number st b1 = +infty ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ext-real number holds
( ( Fx is finite-order & ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st b2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies b1 = b2 ) & ( not Fx is finite-order & b1 = +infty & b2 = +infty implies b1 = b2 ) )
proof
let O1, O2 be ext-real number ; ::_thesis: ( ( Fx is finite-order & ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies O1 = O2 ) & ( not Fx is finite-order & O1 = +infty & O2 = +infty implies O1 = O2 ) )
now__::_thesis:_(_Fx_is_finite-order_&_(_for_Gx_being_Subset-Family_of_X_st_O1_+_1_in_card_Gx_&_Gx_c=_Fx_holds_
meet_Gx_is_empty_)_&_ex_G1_being_Subset-Family_of_X_st_
(_G1_c=_Fx_&_card_G1_=_O1_+_1_&_(_not_meet_G1_is_empty_or_G1_is_empty_)_)_&_(_for_Gx_being_Subset-Family_of_X_st_O2_+_1_in_card_Gx_&_Gx_c=_Fx_holds_
meet_Gx_is_empty_)_&_ex_G2_being_Subset-Family_of_X_st_
(_G2_c=_Fx_&_card_G2_=_O2_+_1_&_(_not_meet_G2_is_empty_or_G2_is_empty_)_)_implies_O1_=_O2_)
assume Fx is finite-order ; ::_thesis: ( ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex G1 being Subset-Family of X st
( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex G2 being Subset-Family of X st
( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )
assume A14: for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ; ::_thesis: ( ex G1 being Subset-Family of X st
( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex G2 being Subset-Family of X st
( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )
given G1 being Subset-Family of X such that A15: G1 c= Fx and
A16: card G1 = O1 + 1 and
A17: ( not meet G1 is empty or G1 is empty ) ; ::_thesis: ( ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex G2 being Subset-Family of X st
( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )
assume A18: for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ; ::_thesis: ( ex G2 being Subset-Family of X st
( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )
given G2 being Subset-Family of X such that A19: G2 c= Fx and
A20: card G2 = O2 + 1 and
A21: ( not meet G2 is empty or G2 is empty ) ; ::_thesis: O1 = O2
not card G2 in card G1 by A15, A17, A18, A20;
then A22: card G1 c= card G2 by CARD_1:3;
not card G1 in card G2 by A14, A16, A19, A21;
then card G1 = card G2 by A22, CARD_1:3;
hence O1 = O2 by A16, A20, XXREAL_3:11; ::_thesis: verum
end;
hence ( ( Fx is finite-order & ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies O1 = O2 ) & ( not Fx is finite-order & O1 = +infty & O2 = +infty implies O1 = O2 ) ) ; ::_thesis: verum
end;
consistency
for b1 being ext-real number holds verum ;
end;
:: deftheorem Def2 defines order TOPDIM_2:def_2_:_
for X being set
for Fx being Subset-Family of X
for b3 being ext-real number holds
( ( Fx is finite-order implies ( b3 = order Fx iff ( ( for Gx being Subset-Family of X st b3 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b3 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b3 = order Fx iff b3 = +infty ) ) );
registration
let X be set ;
let F be finite-order Subset-Family of X;
cluster(order F) + 1 -> natural ;
coherence
(order F) + 1 is natural
proof
consider G being Subset-Family of X such that
A1: G c= F and
A2: card G = (order F) + 1 and
A3: ( not meet G is empty or G is empty ) by Def2;
consider n being Nat such that
A4: for H being Subset-Family of X st H c= F & n in card H holds
meet H is empty by Def1;
card n = card (card n) ;
then A5: card n = n by CARD_1:40;
then not card n in card G by A1, A3, A4;
then card G c= n by A5, CARD_1:4;
then reconsider G = G as finite Subset-Family of X ;
(order F) + 1 = ((card G) - 1) + 1 by A2;
hence (order F) + 1 is natural ; ::_thesis: verum
end;
cluster order F -> ext-real integer ;
coherence
order F is integer
proof
reconsider O1 = (order F) + 1 as Nat ;
(order F) + 1 = (O1 - 1) + 1 ;
hence order F is integer by XXREAL_3:11; ::_thesis: verum
end;
end;
theorem Th1: :: TOPDIM_2:1
for n being Nat
for X being set
for Fx being Subset-Family of X st order Fx <= n holds
Fx is finite-order
proof
let n be Nat; ::_thesis: for X being set
for Fx being Subset-Family of X st order Fx <= n holds
Fx is finite-order
let X be set ; ::_thesis: for Fx being Subset-Family of X st order Fx <= n holds
Fx is finite-order
let Fx be Subset-Family of X; ::_thesis: ( order Fx <= n implies Fx is finite-order )
assume order Fx <= n ; ::_thesis: Fx is finite-order
then order Fx <> +infty by XXREAL_0:4;
hence Fx is finite-order by Def2; ::_thesis: verum
end;
theorem :: TOPDIM_2:2
for n being Nat
for X being set
for Fx being Subset-Family of X st order Fx <= n holds
for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty
proof
let n be Nat; ::_thesis: for X being set
for Fx being Subset-Family of X st order Fx <= n holds
for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty
let X be set ; ::_thesis: for Fx being Subset-Family of X st order Fx <= n holds
for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty
let Fx be Subset-Family of X; ::_thesis: ( order Fx <= n implies for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty )
card (n + 1) = card (card (n + 1)) ;
then A1: card (n + 1) = n + 1 by CARD_1:40;
card (n + 2) = card (card (n + 2)) ;
then A2: card (n + 2) = n + 2 by CARD_1:40;
assume A3: order Fx <= n ; ::_thesis: for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty
then reconsider f = Fx as finite-order Subset-Family of X by Th1;
(order f) + 1 <= n + 1 by A3, XREAL_1:6;
then (order f) + 1 < (n + 1) + 1 by NAT_1:13;
then A4: (order f) + 1 in n + 2 by NAT_1:44;
let Gx be Subset-Family of X; ::_thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty )
assume that
A5: Gx c= Fx and
A6: n + 1 in card Gx ; ::_thesis: meet Gx is empty
nextcard (n + 1) c= card Gx by A6, CARD_3:90;
then card ((n + 1) + 1) c= card Gx by A1, NAT_1:42;
hence meet Gx is empty by A5, A2, A4, Def2; ::_thesis: verum
end;
theorem Th3: :: TOPDIM_2:3
for n being Nat
for X being set
for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ) holds
order Fx <= n
proof
let n be Nat; ::_thesis: for X being set
for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ) holds
order Fx <= n
let X be set ; ::_thesis: for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ) holds
order Fx <= n
let Fx be Subset-Family of X; ::_thesis: ( ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ) implies order Fx <= n )
set n1 = n + 1;
assume A1: for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ; ::_thesis: order Fx <= n
A2: now__::_thesis:_for_Gx_being_Subset-Family_of_X_st_Gx_c=_Fx_&_n_+_1_in_card_Gx_holds_
meet_Gx_is_empty
card (card ((n + 1) + 1)) = card ((n + 1) + 1) ;
then A3: card ((n + 1) + 1) = (n + 1) + 1 by CARD_1:40;
let Gx be Subset-Family of X; ::_thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty )
assume that
A4: Gx c= Fx and
A5: n + 1 in card Gx ; ::_thesis: meet Gx is empty
card (card (n + 1)) = card (n + 1) ;
then card (n + 1) = n + 1 by CARD_1:40;
then nextcard (n + 1) = card ((n + 1) + 1) by NAT_1:42;
then card ((n + 1) + 1) c= card Gx by A5, CARD_3:90;
then consider f being Function such that
A6: ( f is one-to-one & dom f = (n + 1) + 1 ) and
A7: rng f c= Gx by CARD_1:10;
reconsider R = rng f as Subset-Family of X by A7, XBOOLE_1:1;
(n + 1) + 1,R are_equipotent by A6, WELLORD2:def_4;
then A8: (n + 1) + 1 = card R by A3, CARD_1:5;
then reconsider R = R as finite Subset-Family of X ;
n + 1 < card R by A8, NAT_1:13;
then A9: meet R is empty by A1, A4, A7, XBOOLE_1:1;
not R is empty by A8;
then meet Gx c= {} by A7, A9, SETFAM_1:6;
hence meet Gx is empty ; ::_thesis: verum
end;
then reconsider f = Fx as finite-order Subset-Family of X by Def1;
consider Gx being Subset-Family of X such that
A10: Gx c= f and
A11: card Gx = (order f) + 1 and
A12: ( not meet Gx is empty or Gx is empty ) by Def2;
assume order Fx > n ; ::_thesis: contradiction
then (order f) + 1 > n + 1 by XREAL_1:6;
then n + 1 in card Gx by A11, NAT_1:44;
hence contradiction by A2, A10, A12; ::_thesis: verum
end;
begin
Lm1: for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
proof
let T be TopSpace; ::_thesis: for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
let Af be finite-ind Subset of T; ::_thesis: (ind Af) + 1 is Nat
Af in (Seq_of_ind T) . (1 + (ind Af)) by TOPDIM_1:def_5;
then (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def_2;
hence (ind Af) + 1 is Nat ; ::_thesis: verum
end;
Lm2: for n being Nat
for T being TopSpace
for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
proof
let n be Nat; ::_thesis: for T being TopSpace
for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
let T be TopSpace; ::_thesis: for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
let g be SetSequence of T; ::_thesis: ( ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) implies ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) )
assume A1: for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ; ::_thesis: ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
defpred S1[ set , set ] means for n being Nat
for F being Subset-Family of T st n = $1 & F = $2 holds
( union F = g . n & F is closed & F is countable );
A2: for x being set st x in NAT holds
ex y being set st
( y in bool (bool the carrier of T) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in bool (bool the carrier of T) & S1[x,y] ) )
assume x in NAT ; ::_thesis: ex y being set st
( y in bool (bool the carrier of T) & S1[x,y] )
then reconsider n = x as Element of NAT ;
g . n is F_sigma by A1;
then consider y being closed countable Subset-Family of T such that
A3: g . n = union y by TOPGEN_4:def_6;
take y ; ::_thesis: ( y in bool (bool the carrier of T) & S1[x,y] )
thus ( y in bool (bool the carrier of T) & S1[x,y] ) by A3; ::_thesis: verum
end;
consider f being SetSequence of (bool the carrier of T) such that
A4: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
take F = Union f; ::_thesis: ( F is closed & F is finite-ind & ind F <= n & F is countable & Union g = union F )
thus F is closed ::_thesis: ( F is finite-ind & ind F <= n & F is countable & Union g = union F )
proof
let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in F or A is closed )
assume A in F ; ::_thesis: A is closed
then consider n being Element of NAT such that
A5: A in f . n by PROB_1:12;
f . n is closed by A4;
hence A is closed by A5, TOPS_2:def_2; ::_thesis: verum
end;
for A being Subset of T st A in F holds
( A is finite-ind & ind A <= n )
proof
let A be Subset of T; ::_thesis: ( A in F implies ( A is finite-ind & ind A <= n ) )
assume A in F ; ::_thesis: ( A is finite-ind & ind A <= n )
then consider i being Element of NAT such that
A6: A in f . i by PROB_1:12;
union (f . i) = g . i by A4;
then A7: A c= g . i by A6, ZFMISC_1:74;
A8: ind (g . i) <= n by A1;
A9: g . i is finite-ind by A1;
then ind A <= ind (g . i) by A7, TOPDIM_1:19;
hence ( A is finite-ind & ind A <= n ) by A7, A8, A9, TOPDIM_1:19, XXREAL_0:2; ::_thesis: verum
end;
hence ( F is finite-ind & ind F <= n ) by TOPDIM_1:11; ::_thesis: ( F is countable & Union g = union F )
for x being set st x in dom f holds
f . x is countable by A4;
hence F is countable by CARD_4:11; ::_thesis: Union g = union F
thus Union g c= union F :: according to XBOOLE_0:def_10 ::_thesis: union F c= Union g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union g or x in union F )
assume x in Union g ; ::_thesis: x in union F
then consider i being Element of NAT such that
A10: x in g . i by PROB_1:12;
union (f . i) = g . i by A4;
then consider y being set such that
A11: x in y and
A12: y in f . i by A10, TARSKI:def_4;
y in F by A12, PROB_1:12;
hence x in union F by A11, TARSKI:def_4; ::_thesis: verum
end;
thus union F c= Union g ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in Union g )
assume x in union F ; ::_thesis: x in Union g
then consider y being set such that
A13: x in y and
A14: y in F by TARSKI:def_4;
consider i being Element of NAT such that
A15: y in f . i by A14, PROB_1:12;
union (f . i) = g . i by A4;
then x in g . i by A13, A15, TARSKI:def_4;
hence x in Union g by PROB_1:12; ::_thesis: verum
end;
end;
Lm3: for n being Nat
for T being metrizable TopSpace st T is second-countable holds
( ( ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )
proof
let n be Nat; ::_thesis: for T being metrizable TopSpace st T is second-countable holds
( ( ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )
defpred S1[ Nat] means for T being metrizable TopSpace st T is second-countable & T is finite-ind & ind T <= $1 holds
ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= $1 - 1 & ind B <= 0 );
defpred S2[ Nat] means for T being metrizable TopSpace st T is second-countable & ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= $1 ) holds
( T is finite-ind & ind T <= $1 );
A1: for n being Nat st S2[n] holds
S1[n + 1]
proof
defpred S3[ set ] means verum;
let n be Nat; ::_thesis: ( S2[n] implies S1[n + 1] )
assume A2: S2[n] ; ::_thesis: S1[n + 1]
let T be metrizable TopSpace; ::_thesis: ( T is second-countable & T is finite-ind & ind T <= n + 1 implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= (n + 1) - 1 & ind B <= 0 ) )
assume that
A3: T is second-countable and
A4: T is finite-ind and
A5: ind T <= n + 1 ; ::_thesis: ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= (n + 1) - 1 & ind B <= 0 )
consider B being Basis of T such that
A6: for A being Subset of T st A in B holds
( Fr A is finite-ind & ind (Fr A) <= (n + 1) - 1 ) by A4, A5, TOPDIM_1:31;
deffunc H1( Subset of T) -> Element of bool the carrier of T = Fr $1;
consider uB being Basis of T such that
A7: uB c= B and
A8: uB is countable by A3, METRIZTS:24;
defpred S4[ set ] means ( $1 in uB & S3[$1] );
consider S being Subset-Family of T such that
A9: S = { H1(b) where b is Subset of T : S4[b] } from LMOD_7:sch_5();
set uS = union S;
set TS = T | (union S);
A10: [#] (T | (union S)) = union S by PRE_TOPC:def_5;
then reconsider S9 = S as Subset-Family of (T | (union S)) by ZFMISC_1:82;
A11: T | ((union S) `) is second-countable by A3;
for a being Subset of (T | (union S)) st a in S9 holds
( a is finite-ind & ind a <= n )
proof
let a be Subset of (T | (union S)); ::_thesis: ( a in S9 implies ( a is finite-ind & ind a <= n ) )
assume a in S9 ; ::_thesis: ( a is finite-ind & ind a <= n )
then consider b being Subset of T such that
A12: a = H1(b) and
A13: S4[b] by A9;
( Fr b is finite-ind & ind (Fr b) <= (n + 1) - 1 ) by A6, A7, A13;
hence ( a is finite-ind & ind a <= n ) by A12, TOPDIM_1:21; ::_thesis: verum
end;
then A14: ( S9 is finite-ind & ind S9 <= n ) by TOPDIM_1:11;
A15: for p being Point of T
for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & (union S) ` misses Fr W )
proof
let p be Point of T; ::_thesis: for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & (union S) ` misses Fr W )
let U be open Subset of T; ::_thesis: ( p in U implies ex W being open Subset of T st
( p in W & W c= U & (union S) ` misses Fr W ) )
assume p in U ; ::_thesis: ex W being open Subset of T st
( p in W & W c= U & (union S) ` misses Fr W )
then consider a being Subset of T such that
A16: a in uB and
A17: ( p in a & a c= U ) by YELLOW_9:31;
uB c= the topology of T by TOPS_2:64;
then reconsider a = a as open Subset of T by A16, PRE_TOPC:def_2;
take a ; ::_thesis: ( p in a & a c= U & (union S) ` misses Fr a )
H1(a) in S by A9, A16;
then H1(a) c= union S by ZFMISC_1:74;
hence ( p in a & a c= U & (union S) ` misses Fr a ) by A17, SUBSET_1:24; ::_thesis: verum
end;
take union S ; ::_thesis: ex B being Subset of T st
( [#] T = (union S) \/ B & union S misses B & ind (union S) <= (n + 1) - 1 & ind B <= 0 )
take (union S) ` ; ::_thesis: ( [#] T = (union S) \/ ((union S) `) & union S misses (union S) ` & ind (union S) <= (n + 1) - 1 & ind ((union S) `) <= 0 )
A18: card { H1(b) where b is Subset of T : ( b in uB & S3[b] ) } c= card uB from BORSUK_2:sch_1();
card uB c= omega by A8, CARD_3:def_14;
then card S c= omega by A9, A18, XBOOLE_1:1;
then A19: S9 is countable by CARD_3:def_14;
A20: S9 is closed
proof
let a be Subset of (T | (union S)); :: according to TOPS_2:def_2 ::_thesis: ( not a in S9 or a is closed )
assume a in S9 ; ::_thesis: a is closed
then ex b being Subset of T st
( a = H1(b) & S4[b] ) by A9;
hence a is closed by TSEP_1:8; ::_thesis: verum
end;
S9 is Cover of (T | (union S)) by A10, SETFAM_1:def_11;
then ind (T | (union S)) <= n by A2, A3, A14, A19, A20;
hence ( [#] T = (union S) \/ ((union S) `) & union S misses (union S) ` & ind (union S) <= (n + 1) - 1 & ind ((union S) `) <= 0 ) by A4, A11, A15, PRE_TOPC:2, SUBSET_1:23, TOPDIM_1:17, TOPDIM_1:38; ::_thesis: verum
end;
A21: S2[ 0 ] by TOPDIM_1:36;
A22: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A23: S2[n] ; ::_thesis: S2[n + 1]
let T be metrizable TopSpace; ::_thesis: ( T is second-countable & ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n + 1 ) implies ( T is finite-ind & ind T <= n + 1 ) )
assume A24: T is second-countable ; ::_thesis: ( for F being Subset-Family of T holds
( not F is closed or not F is Cover of T or not F is countable or not F is finite-ind or not ind F <= n + 1 ) or ( T is finite-ind & ind T <= n + 1 ) )
given F being Subset-Family of T such that A25: F is closed and
A26: F is Cover of T and
A27: F is countable and
A28: ( F is finite-ind & ind F <= n + 1 ) ; ::_thesis: ( T is finite-ind & ind T <= n + 1 )
percases ( T is empty or not T is empty ) ;
suppose T is empty ; ::_thesis: ( T is finite-ind & ind T <= n + 1 )
hence ( T is finite-ind & ind T <= n + 1 ) by TOPDIM_1:6; ::_thesis: verum
end;
supposeA29: not T is empty ; ::_thesis: ( T is finite-ind & ind T <= n + 1 )
set cT = the carrier of T;
A30: not F is empty by A26, A29, SETFAM_1:45, ZFMISC_1:2;
then consider f being Function of NAT,F such that
A31: rng f = F by A27, CARD_3:96;
dom f = NAT by A30, FUNCT_2:def_1;
then reconsider f = f as SetSequence of T by A31, FUNCT_2:2;
consider g being SetSequence of T such that
A32: union (rng f) = union (rng g) and
A33: for i, j being Nat st i <> j holds
g . i misses g . j and
A34: for n being Nat ex fn being finite Subset-Family of T st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) by TOPDIM_1:33;
defpred S3[ set , set ] means for i being Nat
for A, B being Subset of T st $1 = i & $2 = [A,B] holds
( A \/ B = g . i & A is finite-ind & B is finite-ind & ind A <= n & ind B <= 0 );
A35: for x being set st x in NAT holds
ex y being set st
( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[x,y] ) )
assume x in NAT ; ::_thesis: ex y being set st
( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[x,y] )
then reconsider N = x as Element of NAT ;
reconsider gN = g . N as Subset of T ;
dom f = NAT by FUNCT_2:def_1;
then A36: f . N in F by A31, FUNCT_1:def_3;
then A37: f . N is finite-ind by A28, TOPDIM_1:4;
ex fn being finite Subset-Family of T st
( fn = { (f . i) where i is Element of NAT : i < N } & g . N = (f . N) \ (union fn) ) by A34;
then A38: g . N c= f . N by XBOOLE_1:36;
then A39: g . N is finite-ind by A37, TOPDIM_1:19;
A40: ind (g . N) <= ind (f . N) by A37, A38, TOPDIM_1:19;
ind (f . N) <= n + 1 by A28, A36, TOPDIM_1:11;
then A41: ind (g . N) <= n + 1 by A40, XXREAL_0:2;
ind (T | gN) = ind gN by A39, TOPDIM_1:17;
then consider A, B being Subset of (T | gN) such that
A42: A \/ B = [#] (T | gN) and
A misses B and
A43: ( ind A <= (n + 1) - 1 & ind B <= 0 ) by A1, A23, A24, A39, A41;
A44: A is finite-ind by A39;
[#] (T | gN) = gN by PRE_TOPC:def_5;
then reconsider A9 = A, B9 = B as Subset of T by XBOOLE_1:1;
B is finite-ind by A39;
then A45: ( B9 is finite-ind & ind B9 = ind B ) by TOPDIM_1:22;
take y = [A9,B9]; ::_thesis: ( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[x,y] )
thus y in [:(bool the carrier of T),(bool the carrier of T):] ; ::_thesis: S3[x,y]
let i be Nat; ::_thesis: for A, B being Subset of T st x = i & y = [A,B] holds
( A \/ B = g . i & A is finite-ind & B is finite-ind & ind A <= n & ind B <= 0 )
let a, b be Subset of T; ::_thesis: ( x = i & y = [a,b] implies ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 ) )
assume that
A46: x = i and
A47: y = [a,b] ; ::_thesis: ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 )
A48: a = A9 by A47, XTUPLE_0:1;
A9 \/ B9 = g . i by A42, A46, PRE_TOPC:def_5;
hence ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 ) by A43, A44, A45, A47, A48, TOPDIM_1:22, XTUPLE_0:1; ::_thesis: verum
end;
consider P12 being Function of NAT,[:(bool the carrier of T),(bool the carrier of T):] such that
A49: for x being set st x in NAT holds
S3[x,P12 . x] from FUNCT_2:sch_1(A35);
set P1 = pr1 P12;
set P2 = pr2 P12;
set U1 = Union (pr1 P12);
set U2 = Union (pr2 P12);
set Tu1 = T | (Union (pr1 P12));
set Tu2 = T | (Union (pr2 P12));
reconsider Tu1 = T | (Union (pr1 P12)) as metrizable TopSpace ;
A50: dom (pr1 P12) = NAT by FUNCT_2:def_1;
A51: [#] Tu1 = Union (pr1 P12) by PRE_TOPC:def_5;
then reconsider P1 = pr1 P12 as SetSequence of Tu1 by A50, FUNCT_2:2, ZFMISC_1:82;
reconsider Tu2 = T | (Union (pr2 P12)) as metrizable TopSpace ;
A52: dom (pr2 P12) = NAT by FUNCT_2:def_1;
A53: for i being Nat holds g . i is F_sigma
proof
let i be Nat; ::_thesis: g . i is F_sigma
consider fi being finite Subset-Family of T such that
A54: fi = { (f . j) where j is Element of NAT : j < i } and
A55: g . i = (f . i) \ (union fi) by A34;
fi is closed
proof
let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in fi or A is closed )
assume A in fi ; ::_thesis: A is closed
then A56: ex j being Element of NAT st
( A = f . j & j < i ) by A54;
dom f = NAT by FUNCT_2:def_1;
then A in F by A31, A56, FUNCT_1:def_3;
hence A is closed by A25, TOPS_2:def_2; ::_thesis: verum
end;
then A57: union fi is closed by TOPS_2:21;
( dom f = NAT & i in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
then f . i in F by A31, FUNCT_1:def_3;
then f . i is closed by A25, TOPS_2:def_2;
then A58: f . i is F_sigma by A29, TOPGEN_4:43;
((union fi) `) /\ (f . i) = (([#] T) /\ (f . i)) \ (union fi) by XBOOLE_1:49
.= g . i by A55, XBOOLE_1:28 ;
hence g . i is F_sigma by A29, A57, A58, TOPGEN_4:39; ::_thesis: verum
end;
for i being Nat holds
( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma )
proof
let i be Nat; ::_thesis: ( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma )
consider y1, y2 being set such that
A59: y1 in bool the carrier of T and
A60: y2 in bool the carrier of T and
A61: P12 . i = [y1,y2] by ZFMISC_1:def_2;
reconsider y1 = y1 as Subset of T by A59;
A62: i in NAT by ORDINAL1:def_12;
then A63: ( y1 is finite-ind & ind y1 <= n ) by A49, A60, A61;
( [y1,y2] `1 = y1 & dom P12 = NAT ) by FUNCT_2:def_1;
then A64: y1 = P1 . i by A61, A62, MCART_1:def_12;
A65: (Union (pr1 P12)) /\ (g . i) c= P1 . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union (pr1 P12)) /\ (g . i) or x in P1 . i )
assume A66: x in (Union (pr1 P12)) /\ (g . i) ; ::_thesis: x in P1 . i
then A67: x in g . i by XBOOLE_0:def_4;
x in Union (pr1 P12) by A66, XBOOLE_0:def_4;
then consider j being Element of NAT such that
A68: x in P1 . j by PROB_1:12;
consider z1, z2 being set such that
A69: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and
A70: P12 . j = [z1,z2] by ZFMISC_1:def_2;
( [z1,z2] `1 = z1 & dom P12 = NAT ) by FUNCT_2:def_1;
then A71: z1 = P1 . j by A70, MCART_1:def_12;
z1 \/ z2 = g . j by A49, A69, A70;
then x in g . j by A68, A71, XBOOLE_0:def_3;
then g . i meets g . j by A67, XBOOLE_0:3;
hence x in P1 . i by A33, A68; ::_thesis: verum
end;
y1 \/ y2 = g . i by A49, A60, A61, A62;
then P1 . i c= g . i by A64, XBOOLE_1:7;
then P1 . i c= (Union (pr1 P12)) /\ (g . i) by A51, XBOOLE_1:19;
then ( P1 . i = (Union (pr1 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A65, XBOOLE_0:def_10;
hence ( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma ) by A63, A64, METRIZTS:10, TOPDIM_1:21; ::_thesis: verum
end;
then consider G1 being Subset-Family of Tu1 such that
A72: ( G1 is closed & G1 is finite-ind & ind G1 <= n & G1 is countable ) and
A73: Union P1 = union G1 by Lm2;
A74: G1 is Cover of Tu1 by A51, A73, SETFAM_1:def_11;
then A75: Tu1 is finite-ind by A23, A24, A72;
then A76: Union (pr1 P12) is finite-ind by TOPDIM_1:18;
A77: [#] Tu2 = Union (pr2 P12) by PRE_TOPC:def_5;
then reconsider P2 = pr2 P12 as SetSequence of Tu2 by A52, FUNCT_2:2, ZFMISC_1:82;
for i being Nat holds
( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma )
proof
let i be Nat; ::_thesis: ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma )
consider y1, y2 being set such that
A78: y1 in bool the carrier of T and
A79: y2 in bool the carrier of T and
A80: P12 . i = [y1,y2] by ZFMISC_1:def_2;
reconsider y2 = y2 as Subset of T by A79;
A81: i in NAT by ORDINAL1:def_12;
then A82: ( y2 is finite-ind & ind y2 <= 0 ) by A49, A78, A80;
( [y1,y2] `2 = y2 & dom P12 = NAT ) by FUNCT_2:def_1;
then A83: y2 = P2 . i by A80, A81, MCART_1:def_13;
A84: (Union (pr2 P12)) /\ (g . i) c= P2 . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union (pr2 P12)) /\ (g . i) or x in P2 . i )
assume A85: x in (Union (pr2 P12)) /\ (g . i) ; ::_thesis: x in P2 . i
then A86: x in g . i by XBOOLE_0:def_4;
x in Union (pr2 P12) by A85, XBOOLE_0:def_4;
then consider j being Element of NAT such that
A87: x in P2 . j by PROB_1:12;
consider z1, z2 being set such that
A88: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and
A89: P12 . j = [z1,z2] by ZFMISC_1:def_2;
( [z1,z2] `2 = z2 & dom P12 = NAT ) by FUNCT_2:def_1;
then A90: z2 = P2 . j by A89, MCART_1:def_13;
z1 \/ z2 = g . j by A49, A88, A89;
then x in g . j by A87, A90, XBOOLE_0:def_3;
then g . i meets g . j by A86, XBOOLE_0:3;
hence x in P2 . i by A33, A87; ::_thesis: verum
end;
y1 \/ y2 = g . i by A49, A78, A80, A81;
then P2 . i c= g . i by A83, XBOOLE_1:7;
then P2 . i c= (Union (pr2 P12)) /\ (g . i) by A77, XBOOLE_1:19;
then ( P2 . i = (Union (pr2 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A84, XBOOLE_0:def_10;
hence ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma ) by A82, A83, METRIZTS:10, TOPDIM_1:21; ::_thesis: verum
end;
then consider G2 being Subset-Family of Tu2 such that
A91: ( G2 is closed & G2 is finite-ind & ind G2 <= 0 & G2 is countable ) and
A92: Union P2 = union G2 by Lm2;
A93: G2 is Cover of Tu2 by A77, A92, SETFAM_1:def_11;
then Tu2 is finite-ind by A23, A24, A91;
then A94: Union (pr2 P12) is finite-ind by TOPDIM_1:18;
ind Tu1 <= n by A23, A24, A72, A74;
then ind (Union (pr1 P12)) <= n by A76, TOPDIM_1:17;
then A95: (ind (Union (pr1 P12))) + 1 <= n + 1 by XREAL_1:6;
A96: Union (pr1 P12) is finite-ind by A75, TOPDIM_1:18;
[#] T c= (Union (pr1 P12)) \/ (Union (pr2 P12))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in (Union (pr1 P12)) \/ (Union (pr2 P12)) )
A97: dom P12 = NAT by FUNCT_2:def_1;
assume x in [#] T ; ::_thesis: x in (Union (pr1 P12)) \/ (Union (pr2 P12))
then x in Union g by A26, A31, A32, SETFAM_1:45;
then consider i being Element of NAT such that
A98: x in g . i by PROB_1:12;
consider y1, y2 being set such that
A99: ( y1 in bool the carrier of T & y2 in bool the carrier of T ) and
A100: P12 . i = [y1,y2] by ZFMISC_1:def_2;
[y1,y2] `1 = y1 ;
then A101: y1 = P1 . i by A97, A100, MCART_1:def_12;
[y1,y2] `2 = y2 ;
then A102: y2 = P2 . i by A97, A100, MCART_1:def_13;
y1 \/ y2 = g . i by A49, A99, A100;
then ( x in P1 . i or x in P2 . i ) by A98, A101, A102, XBOOLE_0:def_3;
then ( x in Union (pr1 P12) or x in Union (pr2 P12) ) by PROB_1:12;
hence x in (Union (pr1 P12)) \/ (Union (pr2 P12)) by XBOOLE_0:def_3; ::_thesis: verum
end;
then A103: (Union (pr1 P12)) \/ (Union (pr2 P12)) = [#] T by XBOOLE_0:def_10;
ind Tu2 <= 0 by A24, A91, A93, TOPDIM_1:36;
then A104: ind (Union (pr2 P12)) <= 0 by A94, TOPDIM_1:17;
T | (Union (pr2 P12)) is second-countable by A24;
then ( (Union (pr1 P12)) \/ (Union (pr2 P12)) is finite-ind & ind ((Union (pr1 P12)) \/ (Union (pr2 P12))) <= (ind (Union (pr1 P12))) + 1 ) by A94, A104, A96, TOPDIM_1:40;
hence ( T is finite-ind & ind T <= n + 1 ) by A103, A95, TOPDIM_1:def_4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A105: for n being Nat holds S2[n] from NAT_1:sch_2(A21, A22);
let T be metrizable TopSpace; ::_thesis: ( T is second-countable implies ( ( ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) ) )
assume A106: T is second-countable ; ::_thesis: ( ( ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )
thus ( ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) by A105, A106; ::_thesis: ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) )
assume that
A107: T is finite-ind and
A108: ind T <= n ; ::_thesis: ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )
percases ( n = 0 or n > 0 ) ;
supposeA109: n = 0 ; ::_thesis: ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )
take {} T ; ::_thesis: ex B being Subset of T st
( [#] T = ({} T) \/ B & {} T misses B & ind ({} T) <= n - 1 & ind B <= 0 )
take [#] T ; ::_thesis: ( [#] T = ({} T) \/ ([#] T) & {} T misses [#] T & ind ({} T) <= n - 1 & ind ([#] T) <= 0 )
thus ( [#] T = ({} T) \/ ([#] T) & {} T misses [#] T & ind ({} T) <= n - 1 & ind ([#] T) <= 0 ) by A108, A109, TOPDIM_1:6, XBOOLE_1:65; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
( S2[n1] & n1 + 1 = n ) by A105;
hence ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by A1, A106, A107, A108; ::_thesis: verum
end;
end;
end;
theorem :: TOPDIM_2:4
for n being Nat
for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is closed & F is Cover of TM & F is countable & F is finite-ind & ind F <= n ) holds
( TM is finite-ind & ind TM <= n ) by Lm3;
theorem Th5: :: TOPDIM_2:5
for TM being metrizable TopSpace
for I being Integer
for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds
( ind (A \/ B) <= I & A \/ B is finite-ind )
proof
let TM be metrizable TopSpace; ::_thesis: for I being Integer
for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds
( ind (A \/ B) <= I & A \/ B is finite-ind )
let I be Integer; ::_thesis: for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds
( ind (A \/ B) <= I & A \/ B is finite-ind )
let A, B be finite-ind Subset of TM; ::_thesis: ( A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I implies ( ind (A \/ B) <= I & A \/ B is finite-ind ) )
assume that
A1: A is closed and
A2: TM | (A \/ B) is second-countable and
A3: ind A <= I and
A4: ind B <= I ; ::_thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind )
- 1 <= ind A by TOPDIM_1:5;
then A5: - 1 <= I by A3, XXREAL_0:2;
percases ( A \/ B is empty or not A \/ B is empty ) ;
suppose A \/ B is empty ; ::_thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind )
hence ( ind (A \/ B) <= I & A \/ B is finite-ind ) by A5, TOPDIM_1:6; ::_thesis: verum
end;
supposeA6: not A \/ B is empty ; ::_thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind )
then A7: not TM is empty ;
( not A is empty or not B is empty ) by A6;
then ( 0 <= ind A or 0 <= ind B ) by A7;
then A8: I in NAT by A3, A4, INT_1:3;
reconsider AB = A \/ B as Subset of TM ;
set Tab = TM | AB;
A9: [#] (TM | AB) = AB by PRE_TOPC:def_5;
then reconsider a = A, b = B as Subset of (TM | AB) by XBOOLE_1:7;
A /\ ([#] (TM | AB)) = a by XBOOLE_1:28;
then A10: a is closed by A1, TSP_1:def_2;
then consider F being closed countable Subset-Family of (TM | AB) such that
A11: a ` = union F by TOPGEN_4:def_6;
reconsider a = a, b = b as finite-ind Subset of (TM | AB) by TOPDIM_1:21;
reconsider AA = {a} as Subset-Family of (TM | AB) ;
union (AA \/ F) = (union AA) \/ (union F) by ZFMISC_1:78
.= a \/ (a `) by A11, ZFMISC_1:25
.= [#] (TM | AB) by PRE_TOPC:2 ;
then A12: AA \/ F is Cover of (TM | AB) by SETFAM_1:def_11;
AA is closed
proof
let D be Subset of (TM | AB); :: according to TOPS_2:def_2 ::_thesis: ( not D in AA or D is closed )
assume D in AA ; ::_thesis: D is closed
hence D is closed by A10, TARSKI:def_1; ::_thesis: verum
end;
then A13: AA \/ F is closed by TOPS_2:16;
for D being Subset of (TM | AB) st D in AA \/ F holds
( D is finite-ind & ind D <= I )
proof
let D be Subset of (TM | AB); ::_thesis: ( D in AA \/ F implies ( D is finite-ind & ind D <= I ) )
assume A14: D in AA \/ F ; ::_thesis: ( D is finite-ind & ind D <= I )
percases ( D in AA or D in F ) by A14, XBOOLE_0:def_3;
suppose D in AA ; ::_thesis: ( D is finite-ind & ind D <= I )
then D = a by TARSKI:def_1;
hence ( D is finite-ind & ind D <= I ) by A3, TOPDIM_1:21; ::_thesis: verum
end;
supposeA15: D in F ; ::_thesis: ( D is finite-ind & ind D <= I )
a ` = b \ a by A9, XBOOLE_1:40;
then A16: a ` c= b by XBOOLE_1:36;
D c= a ` by A11, A15, ZFMISC_1:74;
then A17: D c= b by A16, XBOOLE_1:1;
then ( ind b = ind B & ind D <= ind b ) by TOPDIM_1:19, TOPDIM_1:21;
hence ( D is finite-ind & ind D <= I ) by A4, A17, TOPDIM_1:19, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
then A18: ( AA \/ F is finite-ind & ind (AA \/ F) <= I ) by A5, TOPDIM_1:11;
A19: AA \/ F is countable by CARD_2:85;
then TM | AB is finite-ind by A2, A8, A12, A13, A18, Lm3;
then A20: A \/ B is finite-ind by TOPDIM_1:18;
ind (TM | AB) <= I by A2, A8, A12, A13, A18, A19, Lm3;
hence ( ind (A \/ B) <= I & A \/ B is finite-ind ) by A20, TOPDIM_1:17; ::_thesis: verum
end;
end;
end;
theorem :: TOPDIM_2:6
for n being Nat
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds
ex A, B being Subset of TM st
( [#] TM = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by Lm3;
theorem Th7: :: TOPDIM_2:7
for I being Integer
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= I holds
ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
proof
let I be Integer; ::_thesis: for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= I holds
ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
defpred S1[ Nat] means for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= $1 - 1 holds
ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) );
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= I implies ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) ) )
assume that
A1: ( TM is second-countable & TM is finite-ind ) and
A2: ind TM <= I ; ::_thesis: ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
- 1 <= ind ([#] TM) by A1, TOPDIM_1:5;
then - 1 <= I by A2, XXREAL_0:2;
then (- 1) + 1 <= I + 1 by XREAL_1:6;
then reconsider i1 = I + 1 as Element of NAT by INT_1:3;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= (n + 1) - 1 implies ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) ) )
assume that
A5: TM is second-countable and
A6: TM is finite-ind and
A7: ind TM <= (n + 1) - 1 ; ::_thesis: ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
consider A, B being Subset of TM such that
A8: [#] TM = A \/ B and
A9: A misses B and
A10: ind A <= n - 1 and
A11: ind B <= 0 by A5, A6, A7, Lm3;
set BB = {B};
for b being Subset of TM st b in {B} holds
( b is finite-ind & ind b <= 0 ) by A6, A11, TARSKI:def_1;
then A12: ( {B} is finite-ind & ind {B} <= 0 ) by TOPDIM_1:11;
set TA = TM | A;
ind (TM | A) = ind A by A6, TOPDIM_1:17;
then consider F being finite Subset-Family of (TM | A) such that
A13: F is Cover of (TM | A) and
A14: F is finite-ind and
A15: ind F <= 0 and
A16: card F <= n and
A17: for A, B being Subset of (TM | A) st A in F & B in F & A meets B holds
A = B by A4, A5, A6, A10;
[#] (TM | A) c= [#] TM by PRE_TOPC:def_4;
then bool ([#] (TM | A)) c= bool ([#] TM) by ZFMISC_1:67;
then reconsider F9 = F as finite Subset-Family of TM by XBOOLE_1:1;
take G = F9 \/ {B}; ::_thesis: ( G is Cover of TM & G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds
A = B ) )
A18: union F9 = [#] (TM | A) by A13, SETFAM_1:45
.= A by PRE_TOPC:def_5 ;
then union G = A \/ (union {B}) by ZFMISC_1:78
.= [#] TM by A8, ZFMISC_1:25 ;
hence G is Cover of TM by SETFAM_1:def_11; ::_thesis: ( G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds
A = B ) )
( F9 is finite-ind & ind F9 = ind F ) by A14, TOPDIM_1:29;
hence ( G is finite-ind & ind G <= 0 ) by A12, A15, TOPDIM_1:13; ::_thesis: ( card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds
A = B ) )
card {B} = 1 by CARD_1:30;
then A19: card G <= (card F9) + 1 by CARD_2:43;
(card F9) + 1 <= n + 1 by A16, XREAL_1:6;
hence card G <= n + 1 by A19, XXREAL_0:2; ::_thesis: for A, B being Subset of TM st A in G & B in G & A meets B holds
A = B
let a, b be Subset of TM; ::_thesis: ( a in G & b in G & a meets b implies a = b )
assume that
A20: ( a in G & b in G ) and
A21: a meets b ; ::_thesis: a = b
percases ( ( a in F & b in F ) or ( a in F & b in {B} ) or ( a in {B} & b in F ) or ( a in {B} & b in {B} ) ) by A20, XBOOLE_0:def_3;
suppose ( a in F & b in F ) ; ::_thesis: a = b
hence a = b by A17, A21; ::_thesis: verum
end;
supposeA22: ( a in F & b in {B} ) ; ::_thesis: a = b
then b = B by TARSKI:def_1;
hence a = b by A9, A18, A21, A22, XBOOLE_1:63, ZFMISC_1:74; ::_thesis: verum
end;
supposeA23: ( a in {B} & b in F ) ; ::_thesis: a = b
then a = B by TARSKI:def_1;
hence a = b by A9, A18, A21, A23, XBOOLE_1:63, ZFMISC_1:74; ::_thesis: verum
end;
supposeA24: ( a in {B} & b in {B} ) ; ::_thesis: a = b
then a = B by TARSKI:def_1;
hence a = b by A24, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
A25: S1[ 0 ]
proof
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= 0 - 1 implies ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) ) )
assume that
TM is second-countable and
A26: TM is finite-ind and
A27: ind TM <= 0 - 1 ; ::_thesis: ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
ind ([#] TM) >= - 1 by A26, TOPDIM_1:5;
then ind ([#] TM) = - 1 by A27, XXREAL_0:1;
then A28: [#] TM = {} TM by A26, TOPDIM_1:6;
reconsider F = {} as empty Subset-Family of TM by TOPGEN_4:18;
take F ; ::_thesis: ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
F c= {({} TM)} by XBOOLE_1:2;
hence ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) ) by A28, SETFAM_1:def_11, TOPDIM_1:10, ZFMISC_1:2; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A25, A3);
then S1[i1] ;
hence ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) ) by A1, A2; ::_thesis: verum
end;
theorem Th8: :: TOPDIM_2:8
for I being Integer
for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) holds
( TM is finite-ind & ind TM <= I )
proof
let I be Integer; ::_thesis: for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) holds
( TM is finite-ind & ind TM <= I )
defpred S1[ Nat] means for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 ) holds
( TM is finite-ind & ind TM <= $1 - 1 );
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) implies ( TM is finite-ind & ind TM <= I ) )
assume A1: TM is second-countable ; ::_thesis: ( for F being finite Subset-Family of TM holds
( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= I + 1 ) or ( TM is finite-ind & ind TM <= I ) )
given F being finite Subset-Family of TM such that A2: ( F is Cover of TM & F is finite-ind & ind F <= 0 ) and
A3: card F <= I + 1 ; ::_thesis: ( TM is finite-ind & ind TM <= I )
reconsider i1 = I + 1 as Element of NAT by A3, INT_1:3;
A4: S1[ 0 ]
proof
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 ) implies ( TM is finite-ind & ind TM <= 0 - 1 ) )
assume TM is second-countable ; ::_thesis: ( for F being finite Subset-Family of TM holds
( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= 0 ) or ( TM is finite-ind & ind TM <= 0 - 1 ) )
given F being finite Subset-Family of TM such that A5: F is Cover of TM and
F is finite-ind and
ind F <= 0 and
A6: card F <= 0 ; ::_thesis: ( TM is finite-ind & ind TM <= 0 - 1 )
F = {} by A6;
then [#] TM = {} by A5, SETFAM_1:45, ZFMISC_1:2;
hence ( TM is finite-ind & ind TM <= 0 - 1 ) by TOPDIM_1:6, TOPDIM_1:def_4; ::_thesis: verum
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A8: S1[n] ; ::_thesis: S1[n + 1]
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 ) implies ( TM is finite-ind & ind TM <= (n + 1) - 1 ) )
assume A9: TM is second-countable ; ::_thesis: ( for F being finite Subset-Family of TM holds
( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= n + 1 ) or ( TM is finite-ind & ind TM <= (n + 1) - 1 ) )
given F being finite Subset-Family of TM such that A10: F is Cover of TM and
A11: F is finite-ind and
A12: ind F <= 0 and
A13: card F <= n + 1 ; ::_thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 )
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 )
then card F = 0 ;
hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A4, A9, A10, A11, A12; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 )
then consider A being set such that
A14: A in F by XBOOLE_0:def_1;
reconsider A = A as Subset of TM by A14;
set AA = {A};
set FA = F \ {A};
A15: (F \ {A}) \/ {A} = F by A14, ZFMISC_1:116;
A16: [#] TM = union F by A10, SETFAM_1:45
.= (union (F \ {A})) \/ (union {A}) by A15, ZFMISC_1:78
.= (union (F \ {A})) \/ A by ZFMISC_1:25 ;
A17: F \ {A} c= F by XBOOLE_1:36;
then A18: ind (F \ {A}) <= 0 by A11, A12, TOPDIM_1:12;
not A in F \ {A} by ZFMISC_1:56;
then F \ {A} c< F by A14, A17, XBOOLE_0:def_8;
then card (F \ {A}) < n + 1 by A13, CARD_2:48, XXREAL_0:2;
then A19: card (F \ {A}) <= n by NAT_1:13;
reconsider uFA = union (F \ {A}) as Subset of TM ;
set Tu = TM | uFA;
A20: [#] (TM | uFA) = uFA by PRE_TOPC:def_5;
then reconsider FA9 = F \ {A} as Subset-Family of (TM | uFA) by ZFMISC_1:82;
A21: TM | A is second-countable by A9;
F \ {A} is finite-ind by A11, A17, TOPDIM_1:12;
then A22: ( FA9 is finite-ind & ind (F \ {A}) = ind FA9 ) by TOPDIM_1:30;
A23: FA9 is Cover of (TM | uFA) by A20, SETFAM_1:def_11;
then A24: TM | uFA is finite-ind by A8, A9, A18, A19, A22;
then A25: ind (TM | uFA) = ind uFA by A20, TOPDIM_1:22;
ind (TM | uFA) <= n - 1 by A8, A9, A18, A19, A22, A23;
then A26: (ind uFA) + 1 <= (n - 1) + 1 by A25, XREAL_1:6;
A27: uFA is finite-ind by A24, TOPDIM_1:18;
( A is finite-ind & ind A <= 0 ) by A11, A12, A14, TOPDIM_1:11;
then ( [#] TM is finite-ind & ind ([#] TM) <= (ind uFA) + 1 ) by A16, A21, A27, TOPDIM_1:40;
hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A26, TOPDIM_1:def_4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A7);
then S1[i1] ;
hence ( TM is finite-ind & ind TM <= I ) by A1, A2, A3; ::_thesis: verum
end;
Lm4: for TM being metrizable TopSpace
for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds
( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
proof
let TM be metrizable TopSpace; ::_thesis: for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds
( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
let A, B be Subset of TM; ::_thesis: ( A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable implies ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) )
assume that
A1: ( A is finite-ind & B is finite-ind ) and
A2: TM | (A \/ B) is second-countable ; ::_thesis: ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
set AB = A \/ B;
set Tab = TM | (A \/ B);
[#] (TM | (A \/ B)) = A \/ B by PRE_TOPC:def_5;
then reconsider a = A, b = B as Subset of (TM | (A \/ B)) by XBOOLE_1:7;
A3: a is finite-ind by A1, TOPDIM_1:21;
then A4: ind ((TM | (A \/ B)) | a) = ind a by TOPDIM_1:17
.= ind A by A1, TOPDIM_1:21 ;
[#] ((TM | (A \/ B)) | b) c= [#] (TM | (A \/ B)) by PRE_TOPC:def_4;
then A5: bool ([#] ((TM | (A \/ B)) | b)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:67;
A6: b is finite-ind by A1, TOPDIM_1:21;
then consider Fb being finite Subset-Family of ((TM | (A \/ B)) | b) such that
A7: Fb is Cover of ((TM | (A \/ B)) | b) and
A8: Fb is finite-ind and
A9: ind Fb <= 0 and
A10: card Fb <= (ind ((TM | (A \/ B)) | b)) + 1 and
for a9, b9 being Subset of ((TM | (A \/ B)) | b) st a9 in Fb & b9 in Fb & a9 meets b9 holds
a9 = b9 by A2, Th7;
consider Fa being finite Subset-Family of ((TM | (A \/ B)) | a) such that
A11: Fa is Cover of ((TM | (A \/ B)) | a) and
A12: Fa is finite-ind and
A13: ind Fa <= 0 and
A14: card Fa <= (ind ((TM | (A \/ B)) | a)) + 1 and
for a9, b9 being Subset of ((TM | (A \/ B)) | a) st a9 in Fa & b9 in Fa & a9 meets b9 holds
a9 = b9 by A2, A3, Th7;
[#] ((TM | (A \/ B)) | a) c= [#] (TM | (A \/ B)) by PRE_TOPC:def_4;
then bool ([#] ((TM | (A \/ B)) | a)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:67;
then reconsider FA = Fa, FB = Fb as finite Subset-Family of (TM | (A \/ B)) by A5, XBOOLE_1:1;
A15: FB is finite-ind by A8, TOPDIM_1:29;
ind ((TM | (A \/ B)) | b) = ind b by A6, TOPDIM_1:17
.= ind B by A1, TOPDIM_1:21 ;
then ( card (FA \/ FB) <= (card FA) + (card FB) & (card FA) + (card FB) <= ((ind A) + 1) + ((ind B) + 1) ) by A10, A14, A4, CARD_2:43, XREAL_1:7;
then A16: card (FA \/ FB) <= (((ind A) + 1) + (ind B)) + 1 by XXREAL_0:2;
union (FA \/ FB) = (union Fa) \/ (union Fb) by ZFMISC_1:78
.= ([#] ((TM | (A \/ B)) | a)) \/ (union Fb) by A11, SETFAM_1:45
.= ([#] ((TM | (A \/ B)) | a)) \/ ([#] ((TM | (A \/ B)) | b)) by A7, SETFAM_1:45
.= a \/ ([#] ((TM | (A \/ B)) | b)) by PRE_TOPC:def_5
.= a \/ b by PRE_TOPC:def_5
.= [#] (TM | (A \/ B)) by PRE_TOPC:def_5 ;
then A17: FA \/ FB is Cover of (TM | (A \/ B)) by SETFAM_1:def_11;
A18: ind FB = ind Fb by A8, TOPDIM_1:29;
A19: FA is finite-ind by A12, TOPDIM_1:29;
ind FA = ind Fa by A12, TOPDIM_1:29;
then A20: ind (FA \/ FB) <= 0 by A9, A13, A19, A15, A18, TOPDIM_1:13;
then TM | (A \/ B) is finite-ind by A2, A15, A16, A19, A17, Th8;
then A21: A \/ B is finite-ind by TOPDIM_1:18;
ind (TM | (A \/ B)) <= ((ind A) + 1) + (ind B) by A2, A15, A16, A19, A17, A20, Th8;
hence ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by A21, TOPDIM_1:17; ::_thesis: verum
end;
registration
let TM be second-countable metrizable TopSpace;
let A, B be finite-ind Subset of TM;
clusterA \/ B -> finite-ind for Subset of TM;
coherence
for b1 being Subset of TM st b1 = A \/ B holds
b1 is with_finite_small_inductive_dimension
proof
TM | (A \/ B) is second-countable ;
hence for b1 being Subset of TM st b1 = A \/ B holds
b1 is with_finite_small_inductive_dimension by Lm4; ::_thesis: verum
end;
end;
theorem :: TOPDIM_2:9
for TM being metrizable TopSpace
for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds
( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by Lm4;
theorem Th10: :: TOPDIM_2:10
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
proof
let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1
for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
let A2 be Subset of T2; ::_thesis: Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
A1: [:(Cl A1),(Cl A2):] /\ [:(Cl (A1 `)),([#] T2):] = [:((Cl A1) /\ (Cl (A1 `))),((Cl A2) /\ ([#] T2)):] by ZFMISC_1:100
.= [:(Fr A1),(Cl A2):] by XBOOLE_1:28 ;
A2: [:(Cl A1),(Cl A2):] /\ [:([#] T1),(Cl (A2 `)):] = [:((Cl A1) /\ ([#] T1)),((Cl A2) /\ (Cl (A2 `))):] by ZFMISC_1:100
.= [:(Cl A1),(Fr A2):] by XBOOLE_1:28 ;
Cl ([#] T1) = [#] T1 by TOPS_1:2;
then A3: Cl [:([#] T1),(A2 `):] = [:([#] T1),(Cl (A2 `)):] by TOPALG_3:14;
Cl ([#] T2) = [#] T2 by TOPS_1:2;
then A4: Cl [:(A1 `),([#] T2):] = [:(Cl (A1 `)),([#] T2):] by TOPALG_3:14;
Cl ([:A1,A2:] `) = Cl ([:([#] T1),([#] T2):] \ [:A1,A2:]) by BORSUK_1:def_2
.= Cl ([:(([#] T1) \ A1),([#] T2):] \/ [:([#] T1),(([#] T2) \ A2):]) by ZFMISC_1:103
.= [:(Cl (A1 `)),([#] T2):] \/ [:([#] T1),(Cl (A2 `)):] by A4, A3, PRE_TOPC:20 ;
hence Fr [:A1,A2:] = [:(Cl A1),(Cl A2):] /\ ([:(Cl (A1 `)),([#] T2):] \/ [:([#] T1),(Cl (A2 `)):]) by TOPALG_3:14
.= [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] by A1, A2, XBOOLE_1:23 ;
::_thesis: verum
end;
Lm5: for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds
( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
proof
let TM1, TM2 be second-countable finite-ind metrizable TopSpace; ::_thesis: ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )
defpred S1[ Nat] means for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= $1 holds
( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) );
reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let TM1, TM2 be second-countable finite-ind metrizable TopSpace; ::_thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= n + 1 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )
assume that
A3: ( not TM1 is empty or not TM2 is empty ) and
A4: ((ind TM1) + (ind TM2)) + 2 <= n + 1 ; ::_thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
set T12 = [:TM1,TM2:];
percases ( TM1 is empty or TM2 is empty or ( not TM1 is empty & not TM2 is empty ) ) ;
supposeA5: TM1 is empty ; ::_thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
then ind TM1 = - 1 by TOPDIM_1:6;
then 0 + (- 1) <= (ind TM2) + (ind TM1) by A3, XREAL_1:6;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A5, TOPDIM_1:6; ::_thesis: verum
end;
supposeA6: TM2 is empty ; ::_thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
then ind TM2 = - 1 by TOPDIM_1:6;
then 0 + (- 1) <= (ind TM1) + (ind TM2) by A3, XREAL_1:6;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A6, TOPDIM_1:6; ::_thesis: verum
end;
supposeA7: ( not TM1 is empty & not TM2 is empty ) ; ::_thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
then reconsider i1 = ind TM1, i2 = ind TM2 as Nat ;
A8: for p being Point of [:TM1,TM2:]
for U being open Subset of [:TM1,TM2:] st p in U holds
ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )
proof
let p be Point of [:TM1,TM2:]; ::_thesis: for U being open Subset of [:TM1,TM2:] st p in U holds
ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )
let U be open Subset of [:TM1,TM2:]; ::_thesis: ( p in U implies ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 ) )
consider F being Subset-Family of [:TM1,TM2:] such that
A9: U = union F and
A10: for e being set st e in F holds
ex X1 being Subset of TM1 ex X2 being Subset of TM2 st
( e = [:X1,X2:] & X1 is open & X2 is open ) by BORSUK_1:5;
assume p in U ; ::_thesis: ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )
then consider U12 being set such that
A11: p in U12 and
A12: U12 in F by A9, TARSKI:def_4;
A13: U12 c= U by A9, A12, ZFMISC_1:74;
consider U1 being Subset of TM1, U2 being Subset of TM2 such that
A14: U12 = [:U1,U2:] and
A15: U1 is open and
A16: U2 is open by A10, A12;
consider p1, p2 being set such that
A17: p1 in U1 and
A18: p2 in U2 and
A19: p = [p1,p2] by A11, A14, ZFMISC_1:def_2;
reconsider p1 = p1 as Point of TM1 by A17;
consider W1 being open Subset of TM1 such that
A20: p1 in W1 and
A21: W1 c= U1 and
Fr W1 is finite-ind and
A22: ind (Fr W1) <= i1 - 1 by A15, A17, TOPDIM_1:16;
set ClW1 = Cl W1;
A23: ( ind (TM1 | (Cl W1)) = ind (Cl W1) & ind (Cl W1) <= i1 ) by TOPDIM_1:17, TOPDIM_1:19;
reconsider p2 = p2 as Point of TM2 by A18;
consider W2 being open Subset of TM2 such that
A24: p2 in W2 and
A25: W2 c= U2 and
Fr W2 is finite-ind and
A26: ind (Fr W2) <= i2 - 1 by A16, A18, TOPDIM_1:16;
reconsider W12 = [:W1,W2:] as open Subset of [:TM1,TM2:] by BORSUK_1:6;
take W12 ; ::_thesis: ( p in W12 & W12 c= U & Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )
W12 c= U12 by A14, A25, A21, ZFMISC_1:96;
hence ( p in W12 & W12 c= U ) by A13, A19, A24, A20, XBOOLE_1:1, ZFMISC_1:87; ::_thesis: ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )
((i1 + i2) + 1) + 1 <= n + 1 by A4;
then A27: (i1 + i2) + 1 <= n by XREAL_1:6;
set FrW1 = Fr W1;
A28: ind (TM1 | (Fr W1)) = ind (Fr W1) by TOPDIM_1:17;
set ClW2 = Cl W2;
reconsider F1C2 = [:(Fr W1),(Cl W2):] as Subset of [:TM1,TM2:] ;
A29: [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] = [:TM1,TM2:] | F1C2 by BORSUK_3:22;
( ind (TM2 | (Cl W2)) = ind (Cl W2) & ind (Cl W2) <= i2 ) by TOPDIM_1:17, TOPDIM_1:19;
then A30: (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) <= (i1 - 1) + i2 by A22, A28, XREAL_1:7;
then ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= ((i1 + i2) - 1) + 2 by XREAL_1:6;
then A31: ( W2 c= Cl W2 & ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= n ) by A27, PRE_TOPC:18, XXREAL_0:2;
then [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] is finite-ind by A2, A7, A24;
then A32: F1C2 is finite-ind by A29, TOPDIM_1:18;
set FrW2 = Fr W2;
reconsider C1F2 = [:(Cl W1),(Fr W2):] as Subset of [:TM1,TM2:] ;
A33: [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] = [:TM1,TM2:] | C1F2 by BORSUK_3:22;
ind (TM2 | (Fr W2)) = ind (Fr W2) by TOPDIM_1:17;
then A34: (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) <= i1 + (i2 - 1) by A26, A23, XREAL_1:7;
then ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= (i1 + (i2 - 1)) + 2 by XREAL_1:6;
then A35: ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= n by A27, XXREAL_0:2;
( W1 c= Cl W1 & [#] (TM1 | (Cl W1)) = Cl W1 ) by PRE_TOPC:18, PRE_TOPC:def_5;
then A36: not TM1 | (Cl W1) is empty by A20;
then [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] is finite-ind by A2, A35;
then A37: C1F2 is finite-ind by A33, TOPDIM_1:18;
ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) by A2, A35, A36;
then ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (i1 + i2) - 1 by A34, XXREAL_0:2;
then A38: ind C1F2 <= (i1 + i2) - 1 by A33, A37, TOPDIM_1:17;
A39: ( F1C2 is closed & [:TM1,TM2:] | (C1F2 \/ F1C2) is second-countable ) by TOPALG_3:15;
ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) by A2, A7, A24, A31;
then ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (i1 - 1) + i2 by A30, XXREAL_0:2;
then ind F1C2 <= (i1 + i2) - 1 by A29, A32, TOPDIM_1:17;
then ( C1F2 \/ F1C2 is finite-ind & ind (C1F2 \/ F1C2) <= (i1 + i2) - 1 ) by A39, A32, A37, A38, Th5;
hence ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 ) by Th10; ::_thesis: verum
end;
then [:TM1,TM2:] is finite-ind by TOPDIM_1:15;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A8, TOPDIM_1:16; ::_thesis: verum
end;
end;
end;
A40: S1[ 0 ]
proof
let TM1, TM2 be second-countable finite-ind metrizable TopSpace; ::_thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= 0 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )
assume that
A41: ( not TM1 is empty or not TM2 is empty ) and
A42: ((ind TM1) + (ind TM2)) + 2 <= 0 ; ::_thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;
i1 + i2 <= 0 by A42;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A41; ::_thesis: verum
end;
A43: for n being Nat holds S1[n] from NAT_1:sch_2(A40, A1);
((ind TM1) + (ind TM2)) + 2 = i1 + i2 ;
hence ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) ) by A43; ::_thesis: verum
end;
registration
let TM1, TM2 be second-countable finite-ind metrizable TopSpace;
cluster[:TM1,TM2:] -> finite-ind ;
coherence
[:TM1,TM2:] is with_finite_small_inductive_dimension
proof
percases ( ( TM1 is empty & TM2 is empty ) or not TM1 is empty or not TM2 is empty ) ;
suppose ( TM1 is empty & TM2 is empty ) ; ::_thesis: [:TM1,TM2:] is with_finite_small_inductive_dimension
hence [:TM1,TM2:] is with_finite_small_inductive_dimension ; ::_thesis: verum
end;
suppose ( not TM1 is empty or not TM2 is empty ) ; ::_thesis: [:TM1,TM2:] is with_finite_small_inductive_dimension
hence [:TM1,TM2:] is with_finite_small_inductive_dimension by Lm5; ::_thesis: verum
end;
end;
end;
end;
theorem Th11: :: TOPDIM_2:11
for n being Nat
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 )
proof
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
end;
theorem :: TOPDIM_2:12
for n being Nat
for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable & ind TM <= n holds
for A, B being Subset of TM st A is closed & B is closed & A misses B holds
ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 )
proof
let n be Nat; ::_thesis: for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable & ind TM <= n holds
for A, B being Subset of TM st A is closed & B is closed & A misses B holds
ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 )
let TM be metrizable TopSpace; ::_thesis: ( TM is finite-ind & TM is second-countable & ind TM <= n implies for A, B being Subset of TM st A is closed & B is closed & A misses B holds
ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 ) )
assume that
A1: ( TM is finite-ind & TM is second-countable ) and
A2: ind TM <= n ; ::_thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds
ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 )
A3: TM | ([#] TM) is second-countable by A1;
let A, B be Subset of TM; ::_thesis: ( A is closed & B is closed & A misses B implies ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 ) )
assume that
A4: ( A is closed & B is closed ) and
A5: A misses B ; ::_thesis: ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 )
consider L being Subset of TM such that
A6: ( L separates A,B & ind (L /\ ([#] TM)) <= n - 1 ) by A4, A1, A2, A3, A5, Th11;
take L ; ::_thesis: ( L separates A,B & ind L <= n - 1 )
thus ( L separates A,B & ind L <= n - 1 ) by A6, XBOOLE_1:28; ::_thesis: verum
end;
theorem Th13: :: TOPDIM_2:13
for n being 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 ) )
proof
let n be Nat; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: ( ( 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 ::_thesis: ( ( 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 ; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: 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; ::_thesis: ( 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, XBOOLE_1:1, ZFMISC_1:31; ::_thesis: ( 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; ::_thesis: 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 ) ; ::_thesis: ( 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); ::_thesis: 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); ::_thesis: ( 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 ; ::_thesis: 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 ; ::_thesis: ( 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; ::_thesis: ( 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; ::_thesis: 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; ::_thesis: verum
end;
theorem :: TOPDIM_2:14
for n being 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 ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )
proof
let n be Nat; ::_thesis: 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 ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )
let TM be metrizable TopSpace; ::_thesis: for H being Subset of TM st TM | H is second-countable holds
( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )
set cTM = [#] TM;
set TOP = the topology of TM;
let M be Subset of TM; ::_thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ) )
assume A1: TM | M is second-countable ; ::_thesis: ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) )
hereby ::_thesis: ( ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) implies ( M is finite-ind & ind M <= n ) )
defpred S1[ set , set ] means for p being Point of TM
for A being Subset of TM st $1 = [p,A] holds
( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = $2 & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) );
assume A2: ( M is finite-ind & ind M <= n ) ; ::_thesis: ex RNG being Basis of TM st
for B being Subset of TM st B in RNG holds
( M /\ (Fr b4) is finite-ind & ind (M /\ (Fr b4)) <= n - 1 )
A3: for x being set st x in [:([#] TM), the topology of TM:] holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [:([#] TM), the topology of TM:] implies ex y being set st S1[x,y] )
assume A4: x in [:([#] TM), the topology of TM:] ; ::_thesis: ex y being set st S1[x,y]
consider p9, A9 being set such that
A5: p9 in [#] TM and
A6: A9 in the topology of TM and
A7: x = [p9,A9] by A4, ZFMISC_1:def_2;
reconsider A9 = A9 as open Subset of TM by A6, PRE_TOPC:def_2;
reconsider p9 = p9 as Point of TM by A5;
percases ( not p9 in A9 or p9 in A9 ) ;
supposeA8: not p9 in A9 ; ::_thesis: ex y being set st S1[x,y]
take {} TM ; ::_thesis: S1[x, {} TM]
let p be Point of TM; ::_thesis: for A being Subset of TM st x = [p,A] holds
( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )
let A be Subset of TM; ::_thesis: ( x = [p,A] implies ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) )
assume A9: x = [p,A] ; ::_thesis: ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )
p = p9 by A7, A9, XTUPLE_0:1;
hence ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A7, A8, A9, PRE_TOPC:def_2, XTUPLE_0:1; ::_thesis: verum
end;
suppose p9 in A9 ; ::_thesis: ex y being set st S1[x,y]
then consider W being open Subset of TM such that
A10: ( p9 in W & W c= A9 & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A1, A2, Th13;
take W ; ::_thesis: S1[x,W]
let p be Point of TM; ::_thesis: for A being Subset of TM st x = [p,A] holds
( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )
let A be Subset of TM; ::_thesis: ( x = [p,A] implies ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) )
assume A11: x = [p,A] ; ::_thesis: ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )
( p = p9 & A = A9 ) by A7, A11, XTUPLE_0:1;
hence ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A10, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A12: dom f = [:([#] TM), the topology of TM:] and
A13: for x being set st x in [:([#] TM), the topology of TM:] holds
S1[x,f . x] from CLASSES1:sch_1(A3);
A14: rng f c= the topology of TM
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the topology of TM )
assume y in rng f ; ::_thesis: y in the topology of TM
then consider x being set such that
A15: x in dom f and
A16: f . x = y by FUNCT_1:def_3;
ex p, A being set st
( p in [#] TM & A in the topology of TM & x = [p,A] ) by A12, A15, ZFMISC_1:def_2;
hence y in the topology of TM by A12, A13, A15, A16; ::_thesis: verum
end;
then reconsider RNG = rng f as Subset-Family of TM by XBOOLE_1:1;
now__::_thesis:_for_A_being_Subset_of_TM_st_A_is_open_holds_
for_p_being_Point_of_TM_st_p_in_A_holds_
ex_W_being_Subset_of_TM_st_
(_W_in_RNG_&_p_in_W_&_W_c=_A_)
let A be Subset of TM; ::_thesis: ( A is open implies for p being Point of TM st p in A holds
ex W being Subset of TM st
( W in RNG & p in W & W c= A ) )
assume A17: A is open ; ::_thesis: for p being Point of TM st p in A holds
ex W being Subset of TM st
( W in RNG & p in W & W c= A )
A18: A in the topology of TM by A17, PRE_TOPC:def_2;
let p be Point of TM; ::_thesis: ( p in A implies ex W being Subset of TM st
( W in RNG & p in W & W c= A ) )
assume A19: p in A ; ::_thesis: ex W being Subset of TM st
( W in RNG & p in W & W c= A )
A20: [p,A] in [:([#] TM), the topology of TM:] by A18, A19, ZFMISC_1:87;
then consider W being open Subset of TM such that
A21: ( W = f . [p,A] & p in W & W c= A ) and
M /\ (Fr W) is finite-ind and
ind (M /\ (Fr W)) <= n - 1 by A13, A19;
reconsider W = W as Subset of TM ;
take W = W; ::_thesis: ( W in RNG & p in W & W c= A )
thus ( W in RNG & p in W & W c= A ) by A12, A20, A21, FUNCT_1:def_3; ::_thesis: verum
end;
then reconsider RNG = RNG as Basis of TM by A14, YELLOW_9:32;
take RNG = RNG; ::_thesis: for B being Subset of TM st B in RNG holds
( M /\ (Fr b3) is finite-ind & ind (M /\ (Fr b3)) <= n - 1 )
let B be Subset of TM; ::_thesis: ( B in RNG implies ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 ) )
assume B in RNG ; ::_thesis: ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 )
then consider x being set such that
A22: x in dom f and
A23: f . x = B by FUNCT_1:def_3;
consider p, A being set such that
A24: p in [#] TM and
A25: A in the topology of TM and
A26: x = [p,A] by A12, A22, ZFMISC_1:def_2;
reconsider A = A as open Subset of TM by A25, PRE_TOPC:def_2;
percases ( p in A or not p in A ) ;
suppose p in A ; ::_thesis: ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 )
then ex W being open Subset of TM st
( W = f . [p,A] & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A12, A13, A22, A26;
hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A23, A26; ::_thesis: verum
end;
suppose not p in A ; ::_thesis: ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 )
then B = {} TM by A12, A13, A22, A23, A24, A26;
then A27: Fr B = {} by TOPGEN_1:14;
0 - 1 <= n - 1 by XREAL_1:9;
hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A27, TOPDIM_1:6; ::_thesis: verum
end;
end;
end;
given B being Basis of TM such that A28: for A being Subset of TM st A in B holds
( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ; ::_thesis: ( M is finite-ind & 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 )
proof
let p be Point of TM; ::_thesis: 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; ::_thesis: ( 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 A29: p in U ; ::_thesis: 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 )
consider a being Subset of TM such that
A30: a in B and
A31: ( p in a & a c= U ) by A29, YELLOW_9:31;
B c= the topology of TM by TOPS_2:64;
then reconsider a = a as open Subset of TM by A30, PRE_TOPC:def_2;
take a ; ::_thesis: ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 )
thus ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 ) by A28, A30, A31; ::_thesis: verum
end;
hence ( M is finite-ind & ind M <= n ) by A1, Th13; ::_thesis: verum
end;
theorem :: TOPDIM_2:15
for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds
ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) by Lm5;
theorem :: TOPDIM_2:16
for TM2, TM1 being second-countable finite-ind metrizable TopSpace st ind TM2 = 0 holds
ind [:TM1,TM2:] = ind TM1
proof
let TM2, TM1 be second-countable finite-ind metrizable TopSpace; ::_thesis: ( ind TM2 = 0 implies ind [:TM1,TM2:] = ind TM1 )
assume A1: ind TM2 = 0 ; ::_thesis: ind [:TM1,TM2:] = ind TM1
then A2: not TM2 is empty by TOPDIM_1:6;
then A3: ind [:TM1,TM2:] <= (ind TM1) + 0 by A1, Lm5;
set x = the Point of TM2;
reconsider X = { the Point of TM2} as Subset of TM2 by A2, ZFMISC_1:31;
percases ( TM1 is empty or not TM1 is empty ) ;
supposeA4: TM1 is empty ; ::_thesis: ind [:TM1,TM2:] = ind TM1
then ind TM1 = - 1 by TOPDIM_1:6;
hence ind [:TM1,TM2:] = ind TM1 by A4, TOPDIM_1:6; ::_thesis: verum
end;
suppose not TM1 is empty ; ::_thesis: ind [:TM1,TM2:] = ind TM1
then ind [:(TM2 | X),TM1:] = ind TM1 by A2, BORSUK_3:13, TOPDIM_1:25;
then A5: ind [:TM1,(TM2 | X):] = ind TM1 by TOPDIM_1:28;
A6: [:TM1,(TM2 | X):] is SubSpace of [:TM1,TM2:] by BORSUK_3:15;
then [#] [:TM1,(TM2 | X):] c= [#] [:TM1,TM2:] by PRE_TOPC:def_4;
then reconsider cT12 = [#] [:TM1,(TM2 | X):] as Subset of [:TM1,TM2:] ;
[:TM1,(TM2 | X):] = [:TM1,TM2:] | cT12 by A6, PRE_TOPC:def_5;
then ind cT12 = ind TM1 by A5, TOPDIM_1:17;
then ind TM1 <= ind [:TM1,TM2:] by TOPDIM_1:19;
hence ind [:TM1,TM2:] = ind TM1 by A3, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
begin
theorem Th17: :: TOPDIM_2:17
for u being Point of (Euclid 1)
for u1, r being real number st <*u1*> = u holds
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
proof
let u be Point of (Euclid 1); ::_thesis: for u1, r being real number st <*u1*> = u holds
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
let u1, r be real number ; ::_thesis: ( <*u1*> = u implies cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } )
assume A1: <*u1*> = u ; ::_thesis: cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
set E1 = { q where q is Element of (Euclid 1) : dist (u,q) <= r } ;
reconsider u1 = u1 as Real by XREAL_0:def_1;
set R1 = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ;
A2: { q where q is Element of (Euclid 1) : dist (u,q) <= r } c= { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } or x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } )
assume x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } ; ::_thesis: x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
then consider q being Element of (Euclid 1) such that
A3: x = q and
A4: dist (u,q) <= r ;
q is Tuple of 1, REAL by FINSEQ_2:131;
then consider s1 being Real such that
A5: q = <*s1*> by FINSEQ_2:97;
<*u1*> - <*s1*> = <*(u1 - s1)*> by RVSUM_1:29;
then sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2)*> by RVSUM_1:55;
then Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2 by RVSUM_1:73;
then A6: sqrt (Sum (sqr (<*u1*> - <*s1*>))) = abs (u1 - s1) by COMPLEX1:72;
A7: |.(<*u1*> - <*s1*>).| <= r by A1, A4, A5, EUCLID:def_6;
then u1 - s1 <= r by A6, ABSVALUE:5;
then (u1 - s1) + s1 <= r + s1 by XREAL_1:6;
then A8: u1 - r <= (r + s1) - r by XREAL_1:9;
- r <= u1 - s1 by A6, A7, ABSVALUE:5;
then (- r) + s1 <= (u1 - s1) + s1 by XREAL_1:6;
then (s1 - r) + r <= u1 + r by XREAL_1:6;
hence x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by A3, A5, A8; ::_thesis: verum
end;
{ <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } c= { q where q is Element of (Euclid 1) : dist (u,q) <= r }
proof
reconsider eu1 = <*u1*> as Element of REAL 1 by FINSEQ_2:98;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } or x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } )
assume x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ; ::_thesis: x in { q where q is Element of (Euclid 1) : dist (u,q) <= r }
then consider s being Real such that
A9: x = <*s*> and
A10: u1 - r <= s and
A11: s <= u1 + r ;
s - r <= (u1 + r) - r by A11, XREAL_1:9;
then A12: (s + (- r)) - s <= u1 - s by XREAL_1:9;
reconsider es = <*s*> as Element of REAL 1 by FINSEQ_2:98;
reconsider q1 = <*s*> as Element of (Euclid 1) by FINSEQ_2:98;
<*u1*> - <*s*> = <*(u1 - s)*> by RVSUM_1:29;
then sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2)*> by RVSUM_1:55;
then A13: Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2 by RVSUM_1:73;
(u1 - r) + r <= s + r by A10, XREAL_1:6;
then u1 - s <= (s + r) - s by XREAL_1:9;
then abs (u1 - s) <= r by A12, ABSVALUE:5;
then |.(<*u1*> - <*s*>).| <= r by A13, COMPLEX1:72;
then ( the distance of (Euclid 1) . (u,q1) = dist (u,q1) & (Pitag_dist 1) . (eu1,es) <= r ) by EUCLID:def_6;
hence x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } by A1, A9; ::_thesis: verum
end;
then { q where q is Element of (Euclid 1) : dist (u,q) <= r } = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by A2, XBOOLE_0:def_10;
hence cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by METRIC_1:18; ::_thesis: verum
end;
Lm6: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def_8;
theorem Th18: :: TOPDIM_2:18
for U being Point of (TOP-REAL 1)
for u1, r being real number st <*u1*> = U & r > 0 holds
Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
proof
let U be Point of (TOP-REAL 1); ::_thesis: for u1, r being real number st <*u1*> = U & r > 0 holds
Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
let u1, r be real number ; ::_thesis: ( <*u1*> = U & r > 0 implies Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} )
assume that
A1: <*u1*> = U and
A2: r > 0 ; ::_thesis: Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
reconsider u = U as Point of (Euclid 1) by Lm6;
A3: Ball (u,r) = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } by A1, JORDAN2B:27;
Ball (U,r) = Ball (u,r) by TOPREAL9:13;
then Ball (U,r) is open by KURATO_2:1;
then A4: Fr (Ball (U,r)) = (Cl (Ball (U,r))) \ (Ball (U,r)) by TOPS_1:42
.= (cl_Ball (U,r)) \ (Ball (U,r)) by A2, JORDAN:23
.= (cl_Ball (u,r)) \ (Ball (U,r)) by TOPREAL9:14
.= (cl_Ball (u,r)) \ (Ball (u,r)) by TOPREAL9:13 ;
A5: cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by A1, Th17;
thus Fr (Ball (U,r)) c= {<*(u1 - r)*>,<*(u1 + r)*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*(u1 - r)*>,<*(u1 + r)*>} c= Fr (Ball (U,r))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (Ball (U,r)) or x in {<*(u1 - r)*>,<*(u1 + r)*>} )
assume A6: x in Fr (Ball (U,r)) ; ::_thesis: x in {<*(u1 - r)*>,<*(u1 + r)*>}
reconsider X = x as Point of (Euclid 1) by Lm6, A6;
x in cl_Ball (u,r) by A4, A6, XBOOLE_0:def_5;
then consider s being Real such that
A7: x = <*s*> and
A8: u1 - r <= s and
A9: s <= u1 + r by A5;
assume A10: not x in {<*(u1 - r)*>,<*(u1 + r)*>} ; ::_thesis: contradiction
then s <> u1 + r by A7, TARSKI:def_2;
then A11: s < u1 + r by A9, XXREAL_0:1;
s <> u1 - r by A7, A10, TARSKI:def_2;
then u1 - r < s by A8, XXREAL_0:1;
then X in Ball (u,r) by A3, A7, A11;
hence contradiction by A4, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*(u1 - r)*>,<*(u1 + r)*>} or x in Fr (Ball (U,r)) )
assume x in {<*(u1 - r)*>,<*(u1 + r)*>} ; ::_thesis: x in Fr (Ball (U,r))
then A12: ( x = <*(u1 - r)*> or x = <*(u1 + r)*> ) by TARSKI:def_2;
A13: ( u1 - r is Real & u1 + r is Real ) by XREAL_0:def_1;
assume A14: not x in Fr (Ball (U,r)) ; ::_thesis: contradiction
u1 + (- r) <= u1 + r by A2, XREAL_1:6;
then x in cl_Ball (u,r) by A5, A12, A13;
then x in Ball (u,r) by A4, A14, XBOOLE_0:def_5;
then ex s being Real st
( x = <*s*> & u1 - r < s & s < u1 + r ) by A3;
hence contradiction by A12, FINSEQ_1:76; ::_thesis: verum
end;
theorem Th19: :: TOPDIM_2:19
for T being TopSpace
for A being countable Subset of T st T | A is T_4 holds
( A is finite-ind & ind A <= 0 )
proof
let T be TopSpace; ::_thesis: for A being countable Subset of T st T | A is T_4 holds
( A is finite-ind & ind A <= 0 )
let A be countable Subset of T; ::_thesis: ( T | A is T_4 implies ( A is finite-ind & ind A <= 0 ) )
assume A1: T | A is T_4 ; ::_thesis: ( A is finite-ind & ind A <= 0 )
percases ( A = {} T or not A is empty ) ;
suppose A = {} T ; ::_thesis: ( A is finite-ind & ind A <= 0 )
hence ( A is finite-ind & ind A <= 0 ) by TOPDIM_1:6; ::_thesis: verum
end;
supposeA2: not A is empty ; ::_thesis: ( A is finite-ind & ind A <= 0 )
then reconsider TT = T as non empty TopSpace ;
reconsider a = A as non empty Subset of TT by A2;
set Ta = TT | a;
deffunc H1( Point of (TT | a)) -> Element of bool the carrier of (TT | a) = {$1};
defpred S1[ set ] means verum;
defpred S2[ set ] means ( $1 in A & S1[$1] );
consider S being Subset-Family of (TT | a) such that
A3: S = { H1(w) where w is Point of (TT | a) : S2[w] } from LMOD_7:sch_5();
for B being Subset of (TT | a) st B in S holds
( B is finite-ind & ind B <= 0 )
proof
let B be Subset of (TT | a); ::_thesis: ( B in S implies ( B is finite-ind & ind B <= 0 ) )
assume B in S ; ::_thesis: ( B is finite-ind & ind B <= 0 )
then consider w being Point of (TT | a) such that
A4: B = H1(w) and
S2[w] by A3;
card H1(w) = 1 by CARD_1:30;
then ind H1(w) < 1 + 0 by TOPDIM_1:8;
hence ( B is finite-ind & ind B <= 0 ) by A4, INT_1:7; ::_thesis: verum
end;
then A5: ( S is finite-ind & ind S <= 0 ) by TOPDIM_1:11;
[#] (TT | a) c= union S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (TT | a) or x in union S )
assume A6: x in [#] (TT | a) ; ::_thesis: x in union S
then x in a by PRE_TOPC:def_5;
then ( x in {x} & {x} in S ) by A3, A6, TARSKI:def_1;
hence x in union S by TARSKI:def_4; ::_thesis: verum
end;
then A7: S is Cover of (TT | a) by SETFAM_1:def_11;
A8: S is closed
proof
let B be Subset of (TT | a); :: according to TOPS_2:def_2 ::_thesis: ( not B in S or B is closed )
assume B in S ; ::_thesis: B is closed
then ex w being Point of (TT | a) st
( B = H1(w) & S2[w] ) by A3;
hence B is closed by A1; ::_thesis: verum
end;
A9: card A c= omega by CARD_3:def_14;
card { H1(w) where w is Point of (TT | a) : S2[w] } c= card A from BORSUK_2:sch_1();
then card S c= omega by A3, A9, XBOOLE_1:1;
then A10: S is countable by CARD_3:def_14;
[#] (TT | a) = A by PRE_TOPC:def_5;
then A11: TT | a is countable by ORDERS_4:def_2;
then TT | a is finite-ind by A1, A5, A7, A8, A10, TOPDIM_1:36;
then A12: A is finite-ind by TOPDIM_1:18;
ind (TT | a) <= 0 by A1, A5, A7, A8, A10, A11, TOPDIM_1:36;
hence ( A is finite-ind & ind A <= 0 ) by A12, TOPDIM_1:17; ::_thesis: verum
end;
end;
end;
registration
let TM be metrizable TopSpace;
cluster countable -> finite-ind for Element of bool the carrier of TM;
coherence
for b1 being Subset of TM st b1 is countable holds
b1 is finite-ind
proof
let A be Subset of TM; ::_thesis: ( A is countable implies A is finite-ind )
assume A1: A is countable ; ::_thesis: A is finite-ind
TM | A is T_4 ;
hence A is finite-ind by A1, Th19; ::_thesis: verum
end;
end;
Lm7: ( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 )
proof
set T = TOP-REAL 0;
TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) = TopSpaceMetr (Euclid 0) by EUCLID:def_8;
then A1: [#] (TOP-REAL 0) = {(<*> REAL)} by FINSEQ_2:94;
card {(<*> REAL)} = 1 by CARD_1:30;
then ind ([#] (TOP-REAL 0)) < 1 by A1, TOPDIM_1:8;
hence ( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 ) by A1, NAT_1:25, TOPDIM_1:def_4; ::_thesis: verum
end;
Lm8: ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 )
proof
set T = TOP-REAL 1;
A1: for p being Point of (TOP-REAL 1)
for U being open Subset of (TOP-REAL 1) st p in U holds
ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )
proof
let p be Point of (TOP-REAL 1); ::_thesis: for U being open Subset of (TOP-REAL 1) st p in U holds
ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )
let U be open Subset of (TOP-REAL 1); ::_thesis: ( p in U implies ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) )
assume A2: p in U ; ::_thesis: ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 )
reconsider p9 = p as Point of (Euclid 1) by Lm6;
set M = Euclid 1;
A3: TopStruct(# the carrier of (TopSpaceMetr (Euclid 1)), the topology of (TopSpaceMetr (Euclid 1)) #) = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def_8;
then reconsider V = U as Subset of (TopSpaceMetr (Euclid 1)) ;
V is open by A3, PRE_TOPC:30;
then consider r being real number such that
A4: r > 0 and
A5: Ball (p9,r) c= U by A2, TOPMETR:15;
reconsider B = Ball (p9,r) as open Subset of (TOP-REAL 1) by KURATO_2:1;
take B ; ::_thesis: ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 )
p9 is Tuple of 1, REAL by FINSEQ_2:131;
then consider p1 being Real such that
A6: p9 = <*p1*> by FINSEQ_2:97;
A7: Ball (p,r) = Ball (p9,r) by TOPREAL9:13;
then A8: Fr B = {<*(p1 - r)*>,<*(p1 + r)*>} by A4, A6, Th18;
TOP-REAL 1 is metrizable
proof
ex f being Function of [: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):],REAL st
( f is_metric_of the carrier of (TOP-REAL 1) & Family_open_set (SpaceMetr ( the carrier of (TOP-REAL 1),f)) = the topology of (TOP-REAL 1) ) by A3, PCOMPS_1:def_8;
hence TOP-REAL 1 is metrizable by PCOMPS_1:def_8; ::_thesis: verum
end;
then (TOP-REAL 1) | (Fr B) is metrizable ;
hence ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 ) by A4, A5, A7, Th19, A8, JORDAN:16; ::_thesis: verum
end;
then A9: TOP-REAL 1 is finite-ind by TOPDIM_1:15;
A10: ind (TOP-REAL 1) >= 1
proof
reconsider p = <*0*>, q = <*1*> as Point of (Euclid 1) by FINSEQ_2:98;
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8;
then reconsider p9 = p as Point of (TOP-REAL 1) ;
A11: Ball (p,1) = Ball (p9,1) by TOPREAL9:13;
then reconsider B = Ball (p9,1) as open Subset of (TOP-REAL 1) by KURATO_2:1;
assume ind (TOP-REAL 1) < 1 ; ::_thesis: contradiction
then ind (TOP-REAL 1) < 1 + 0 ;
then A12: ind (TOP-REAL 1) <= 0 by INT_1:7;
p in B by JORDAN:16;
then consider W being open Subset of (TOP-REAL 1) such that
A13: p in W and
A14: W c= B and
A15: ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by A9, A12, TOPDIM_1:16;
Fr W = {} (TOP-REAL 1) by A15;
then A16: W is closed by TOPGEN_1:14;
A17: W \/ (W `) = [#] (TOP-REAL 1) by PRE_TOPC:2;
W misses W ` by SUBSET_1:24;
then ( [#] (TOP-REAL 1) is convex & W,W ` are_separated ) by A16, CONNSP_1:2;
then A18: W ` = {} (TOP-REAL 1) by A13, A17, CONNSP_1:15;
A19: B = { <*s*> where s is Real : ( 0 - 1 < s & s < 0 + 1 ) } by A11, JORDAN2B:27;
A20: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8;
not q in B
proof
assume q in B ; ::_thesis: contradiction
then ex s being Real st
( q = <*s*> & 0 - 1 < s & s < 0 + 1 ) by A19;
hence contradiction by FINSEQ_1:76; ::_thesis: verum
end;
then not q in W by A14;
hence contradiction by A20, A18, XBOOLE_0:def_5; ::_thesis: verum
end;
ind (TOP-REAL 1) <= 1 by A1, A9, TOPDIM_1:16;
hence ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 ) by A1, A10, TOPDIM_1:15, XXREAL_0:1; ::_thesis: verum
end;
Lm9: for n being Nat holds
( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n )
proof
let n be Nat; ::_thesis: ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n )
defpred S1[ Nat] means ( TOP-REAL $1 is finite-ind & ind (TOP-REAL $1) <= $1 );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
A2: ( TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) & TopStruct(# the carrier of (TOP-REAL (n + 1)), the topology of (TOP-REAL (n + 1)) #) = TopSpaceMetr (Euclid (n + 1)) & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) ) by EUCLID:def_8;
A3: n in NAT by ORDINAL1:def_12;
then A4: [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):], TopSpaceMetr (Euclid (n + 1)) are_homeomorphic by TOPREAL7:25;
TOP-REAL 1, TopSpaceMetr (Euclid 1) are_homeomorphic by A2, YELLOW14:19;
then A5: ( TopSpaceMetr (Euclid 1) is finite-ind & ind (TopSpaceMetr (Euclid 1)) = 1 ) by Lm8, TOPDIM_1:24, TOPDIM_1:25;
assume A6: S1[n] ; ::_thesis: S1[n + 1]
A7: TOP-REAL n, TopSpaceMetr (Euclid n) are_homeomorphic by A2, YELLOW14:19;
A8: TOP-REAL (n + 1), TopSpaceMetr (Euclid (n + 1)) are_homeomorphic by A2, YELLOW14:19;
A9: ( TopSpaceMetr (Euclid n) is finite-ind & ind (TopSpaceMetr (Euclid n)) = ind (TOP-REAL n) ) by A6, A7, TOPDIM_1:24, TOPDIM_1:25;
then A10: ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= (ind (TopSpaceMetr (Euclid n))) + 1 by Lm5, A2, A5;
(ind (TopSpaceMetr (Euclid n))) + 1 <= n + 1 by A6, A9, XREAL_1:6;
then ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= n + 1 by A10, XXREAL_0:2;
then A11: ind (TopSpaceMetr (Euclid (n + 1))) <= n + 1 by A3, A9, A5, A2, TOPDIM_1:25, TOPREAL7:25;
TopSpaceMetr (Euclid (n + 1)) is finite-ind by A9, A5, A2, A4, TOPDIM_1:24;
then TOP-REAL (n + 1) is finite-ind by A8, TOPDIM_1:24;
hence S1[n + 1] by A11, A2, TOPDIM_1:25, YELLOW14:19; ::_thesis: verum
end;
A12: S1[ 0 ] by Lm7;
for n being Nat holds S1[n] from NAT_1:sch_2(A12, A1);
hence ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n ) ; ::_thesis: verum
end;
registration
let n be Nat;
cluster TOP-REAL n -> finite-ind ;
coherence
TOP-REAL n is with_finite_small_inductive_dimension by Lm9;
end;
theorem :: TOPDIM_2:20
for n being Nat st n <= 1 holds
ind (TOP-REAL n) = n
proof
let n be Nat; ::_thesis: ( n <= 1 implies ind (TOP-REAL n) = n )
assume n <= 1 ; ::_thesis: ind (TOP-REAL n) = n
then ( n < 1 or n = 1 ) by XXREAL_0:1;
then ( n = 0 or n = 1 ) by NAT_1:14;
hence ind (TOP-REAL n) = n by Lm7, Lm8; ::_thesis: verum
end;
theorem :: TOPDIM_2:21
for n being Nat holds ind (TOP-REAL n) <= n by Lm9;
Lm10: for TM being metrizable TopSpace
for A being finite-ind Subset of TM st TM | A is second-countable & ind (TM | A) <= 0 holds
for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
proof
let TM be metrizable TopSpace; ::_thesis: for A being finite-ind Subset of TM st TM | A is second-countable & ind (TM | A) <= 0 holds
for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
let A be finite-ind Subset of TM; ::_thesis: ( TM | A is second-countable & ind (TM | A) <= 0 implies for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) )
assume A1: ( TM | A is second-countable & ind (TM | A) <= 0 ) ; ::_thesis: for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
let U1, U2 be open Subset of TM; ::_thesis: ( A c= U1 \/ U2 implies ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) )
assume A2: A c= U1 \/ U2 ; ::_thesis: ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
set U12 = U1 \/ U2;
set TU = TM | (U1 \/ U2);
A3: [#] (TM | (U1 \/ U2)) = U1 \/ U2 by PRE_TOPC:def_5;
then reconsider u1 = U1, u2 = U2, a = A as Subset of (TM | (U1 \/ U2)) by A2, XBOOLE_1:7;
A4: a is finite-ind by TOPDIM_1:21;
A5: u1 ` misses u2 `
proof
assume u1 ` meets u2 ` ; ::_thesis: contradiction
then consider z being set such that
A6: z in u1 ` and
A7: z in u2 ` by XBOOLE_0:3;
( not z in U1 & not z in U2 ) by A6, A7, XBOOLE_0:def_5;
hence contradiction by A3, A6, XBOOLE_0:def_3; ::_thesis: verum
end;
U2 /\ (U1 \/ U2) = u2 by XBOOLE_1:7, XBOOLE_1:28;
then A8: u2 is open by A3, TSP_1:def_1;
U1 /\ (U1 \/ U2) = u1 by XBOOLE_1:7, XBOOLE_1:28;
then A9: u1 is open by A3, TSP_1:def_1;
A10: ind a = ind A by TOPDIM_1:21;
( ind A <= 0 & (TM | (U1 \/ U2)) | a is second-countable ) by A1, METRIZTS:9, TOPDIM_1:17;
then consider L being Subset of (TM | (U1 \/ U2)) such that
A11: L separates u1 ` ,u2 ` and
A12: ind (L /\ a) <= 0 - 1 by A4, A5, A9, A8, A10, Th11;
consider v1, v2 being open Subset of (TM | (U1 \/ U2)) such that
A13: ( u1 ` c= v1 & u2 ` c= v2 ) and
A14: v1 misses v2 and
A15: L = (v1 \/ v2) ` by A11, METRIZTS:def_3;
reconsider V1 = v1, V2 = v2 as Subset of TM by A3, XBOOLE_1:1;
reconsider V1 = V1, V2 = V2 as open Subset of TM by A3, TSEP_1:9;
take V2 ; ::_thesis: ex V2 being open Subset of TM st
( V2 c= U1 & V2 c= U2 & V2 misses V2 & A c= V2 \/ V2 )
take V1 ; ::_thesis: ( V2 c= U1 & V1 c= U2 & V2 misses V1 & A c= V2 \/ V1 )
( u1 ` misses v2 & u2 ` misses v1 ) by A13, A14, XBOOLE_1:63;
hence ( V2 c= U1 & V1 c= U2 & V2 misses V1 ) by A14, SUBSET_1:24; ::_thesis: A c= V2 \/ V1
L /\ a c= a by XBOOLE_1:17;
then A16: L /\ a is finite-ind by A4, TOPDIM_1:19;
then ind (L /\ a) >= - 1 by TOPDIM_1:5;
then ind (L /\ a) = - 1 by A12, XXREAL_0:1;
then L /\ a is empty by A16, TOPDIM_1:6;
then L misses a by XBOOLE_0:def_7;
hence A c= V2 \/ V1 by A15, SUBSET_1:24; ::_thesis: verum
end;
theorem Th22: :: TOPDIM_2:22
for TM being metrizable TopSpace
for A being Subset of TM st TM | A is second-countable & TM | A is finite-ind & ind A <= 0 holds
for F being finite Subset-Family of TM st F is open & F is Cover of A holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
proof
let TM be metrizable TopSpace; ::_thesis: for A being Subset of TM st TM | A is second-countable & TM | A is finite-ind & ind A <= 0 holds
for F being finite Subset-Family of TM st F is open & F is Cover of A holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
defpred S1[ Nat] means for A being Subset of TM st TM | A is second-countable & A is finite-ind & ind A <= 0 holds
for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= $1 holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) );
let A be Subset of TM; ::_thesis: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) )
assume A1: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 ) ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of A implies ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) )
assume A2: ( F is open & F is Cover of A ) ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
let A be Subset of TM; ::_thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) )
assume that
A5: TM | A is second-countable and
A6: A is finite-ind and
A7: ind A <= 0 ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of A & card F <= n + 1 implies ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) )
assume that
A8: F is open and
A9: F is Cover of A and
A10: card F <= n + 1 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
percases ( card F <= n or card F = n + 1 ) by A10, NAT_1:8;
suppose card F <= n ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
hence ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A4, A5, A6, A7, A8, A9; ::_thesis: verum
end;
supposeA11: card F = n + 1 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
then consider x being set such that
A12: F = {x} by A11, CARD_2:42;
set g = F --> x;
( dom (F --> x) = F & rng (F --> x) = F ) by A12, FUNCOP_1:8, FUNCOP_1:13;
then reconsider g = F --> x as Function of F,(bool the carrier of TM) by FUNCT_2:2;
take g ; ::_thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
thus ( rng g is open & rng g is Cover of A ) by A8, A9, A12, FUNCOP_1:8; ::_thesis: ( ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
hereby ::_thesis: for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b
let a be set ; ::_thesis: ( a in F implies g . a c= a )
assume A13: a in F ; ::_thesis: g . a c= a
then g . a = x by FUNCOP_1:7;
hence g . a c= a by A12, A13, TARSKI:def_1; ::_thesis: verum
end;
let a, b be set ; ::_thesis: ( a in F & b in F & a <> b implies g . a misses g . b )
assume that
A14: a in F and
A15: ( b in F & a <> b ) ; ::_thesis: g . a misses g . b
x = a by A12, A14, TARSKI:def_1;
hence g . a misses g . b by A12, A15, TARSKI:def_1; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
not F is empty by A11;
then consider x being set such that
A16: x in F by XBOOLE_0:def_1;
A17: card (F \ {x}) = n1 + 1 by A11, A16, STIRL2_1:55;
then not F \ {x} is empty ;
then consider y being set such that
A18: y in F \ {x} by XBOOLE_0:def_1;
y in F by A18, XBOOLE_0:def_5;
then reconsider x = x, y = y as open Subset of TM by A8, A16, TOPS_2:def_1;
set X = {x};
set xy = x \/ y;
set Y = {y};
set XY = {(x \/ y)};
A19: (F \ {x}) \/ {x} = F by A16, ZFMISC_1:116;
set Fxy = (F \ {x}) \ {y};
A20: card ((F \ {x}) \ {y}) = n1 by A17, A18, STIRL2_1:55;
set FXY = ((F \ {x}) \ {y}) \/ {(x \/ y)};
card {(x \/ y)} = 1 by CARD_1:30;
then A21: card (((F \ {x}) \ {y}) \/ {(x \/ y)}) <= n1 + 1 by A20, CARD_2:43;
F \ {x} is open by A8, TOPS_2:15;
then A22: (F \ {x}) \ {y} is open by TOPS_2:15;
A23: ((F \ {x}) \ {y}) \/ {y} = F \ {x} by A18, ZFMISC_1:116;
for A being Subset of TM st A in {(x \/ y)} holds
A is open by TARSKI:def_1;
then A24: {(x \/ y)} is open by TOPS_2:def_1;
percases ( (F \ {x}) \ {y} is Cover of A or not (F \ {x}) \ {y} is Cover of A ) ;
supposeA25: (F \ {x}) \ {y} is Cover of A ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
card ((F \ {x}) \ {y}) <= n1 + 1 by A20, NAT_1:13;
then consider g being Function of ((F \ {x}) \ {y}),(bool the carrier of TM) such that
A26: rng g is open and
A27: rng g is Cover of A and
A28: for a being set st a in (F \ {x}) \ {y} holds
g . a c= a and
A29: for a, b being set st a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} & a <> b holds
g . a misses g . b by A4, A5, A6, A7, A22, A25;
A30: A c= union (rng g) by A27, SETFAM_1:def_11;
set h = (x,y) --> (({} TM),({} TM));
A31: dom ((x,y) --> (({} TM),({} TM))) = {x,y} by FUNCT_4:62;
not x in F \ {x} by ZFMISC_1:56;
then A32: not x in (F \ {x}) \ {y} by ZFMISC_1:56;
not y in (F \ {x}) \ {y} by ZFMISC_1:56;
then A33: (F \ {x}) \ {y} misses {x,y} by A32, ZFMISC_1:51;
A34: x <> y by A18, ZFMISC_1:56;
then A35: rng ((x,y) --> (({} TM),({} TM))) = {({} TM),({} TM)} by FUNCT_4:64;
A36: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1
.= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4
.= F by A18, A19, ZFMISC_1:116 ;
A37: dom g = (F \ {x}) \ {y} by FUNCT_2:def_1;
then A38: rng (g +* ((x,y) --> (({} TM),({} TM)))) = (rng g) \/ (rng ((x,y) --> (({} TM),({} TM)))) by A31, A33, NECKLACE:6;
dom (g +* ((x,y) --> (({} TM),({} TM)))) = ((F \ {x}) \ {y}) \/ {x,y} by A31, A37, FUNCT_4:def_1;
then reconsider gh = g +* ((x,y) --> (({} TM),({} TM))) as Function of F,(bool the carrier of TM) by A36, A38, FUNCT_2:2;
take gh ; ::_thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds
gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b ) )
( ((x,y) --> (({} TM),({} TM))) . y = {} TM & y in {x,y} ) by FUNCT_4:63, TARSKI:def_2;
then A39: gh . y = {} TM by A31, FUNCT_4:13;
for A being Subset of TM st A in {({} TM),({} TM)} holds
A is open by TARSKI:def_2;
then {({} TM),({} TM)} is open by TOPS_2:def_1;
hence rng gh is open by A26, A35, A38, TOPS_2:13; ::_thesis: ( rng gh is Cover of A & ( for a being set st a in F holds
gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b ) )
union (rng gh) = (union (rng g)) \/ (union (rng ((x,y) --> (({} TM),({} TM))))) by A38, ZFMISC_1:78
.= (union (rng g)) \/ (union {({} TM)}) by A35, ENUMSET1:29
.= (union (rng g)) \/ ({} TM) by ZFMISC_1:25
.= union (rng g) ;
hence rng gh is Cover of A by A30, SETFAM_1:def_11; ::_thesis: ( ( for a being set st a in F holds
gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b ) )
( x in {x,y} & ((x,y) --> (({} TM),({} TM))) . x = {} TM ) by A34, FUNCT_4:63, TARSKI:def_2;
then A40: gh . x = {} TM by A31, FUNCT_4:13;
hereby ::_thesis: for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b
let a be set ; ::_thesis: ( a in F implies gh . b1 c= b1 )
assume A41: a in F ; ::_thesis: gh . b1 c= b1
percases ( a in (F \ {x}) \ {y} or a in {x,y} ) by A36, A41, XBOOLE_0:def_3;
suppose a in (F \ {x}) \ {y} ; ::_thesis: gh . b1 c= b1
then ( not a in dom ((x,y) --> (({} TM),({} TM))) & g . a c= a ) by A28, A33, XBOOLE_0:3;
hence gh . a c= a by FUNCT_4:11; ::_thesis: verum
end;
suppose a in {x,y} ; ::_thesis: gh . b1 c= b1
then ( a = x or a = y ) by TARSKI:def_2;
hence gh . a c= a by A39, A40, XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
let a, b be set ; ::_thesis: ( a in F & b in F & a <> b implies gh . a misses gh . b )
assume that
A42: ( a in F & b in F ) and
A43: a <> b ; ::_thesis: gh . a misses gh . b
percases ( ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) or a in {x,y} or b in {x,y} ) by A36, A42, XBOOLE_0:def_3;
supposeA44: ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) ; ::_thesis: gh . a misses gh . b
then not a in dom ((x,y) --> (({} TM),({} TM))) by A33, XBOOLE_0:3;
then A45: gh . a = g . a by FUNCT_4:11;
( not b in dom ((x,y) --> (({} TM),({} TM))) & g . a misses g . b ) by A29, A33, A43, A44, XBOOLE_0:3;
hence gh . a misses gh . b by A45, FUNCT_4:11; ::_thesis: verum
end;
suppose ( a in {x,y} or b in {x,y} ) ; ::_thesis: gh . a misses gh . b
then ( gh . a = {} TM or gh . b = {} TM ) by A39, A40, TARSKI:def_2;
hence gh . a misses gh . b by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
supposeA46: (F \ {x}) \ {y} is not Cover of A ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
A47: (union ((F \ {x}) \ {y})) \/ (x \/ y) = (union ((F \ {x}) \ {y})) \/ (union {(x \/ y)}) by ZFMISC_1:25
.= union (((F \ {x}) \ {y}) \/ {(x \/ y)}) by ZFMISC_1:78 ;
A48: ((F \ {x}) \ {y}) \/ {(x \/ y)} is open by A22, A24, TOPS_2:13;
A49: union F = (union (F \ {x})) \/ (union {x}) by A19, ZFMISC_1:78
.= (union (F \ {x})) \/ x by ZFMISC_1:25
.= ((union ((F \ {x}) \ {y})) \/ (union {y})) \/ x by A23, ZFMISC_1:78
.= ((union ((F \ {x}) \ {y})) \/ y) \/ x by ZFMISC_1:25
.= (union ((F \ {x}) \ {y})) \/ (y \/ x) by XBOOLE_1:4 ;
A c= union F by A9, SETFAM_1:def_11;
then ((F \ {x}) \ {y}) \/ {(x \/ y)} is Cover of A by A47, A49, SETFAM_1:def_11;
then consider g being Function of (((F \ {x}) \ {y}) \/ {(x \/ y)}),(bool the carrier of TM) such that
A50: rng g is open and
A51: rng g is Cover of A and
A52: for a being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} holds
g . a c= a and
A53: for a, b being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} & b in ((F \ {x}) \ {y}) \/ {(x \/ y)} & a <> b holds
g . a misses g . b by A4, A5, A6, A7, A21, A48;
A54: rng (g | ((F \ {x}) \ {y})) is open by A50, RELAT_1:70, TOPS_2:11;
x \/ y in {(x \/ y)} by TARSKI:def_1;
then A55: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def_3;
then A56: g . (x \/ y) c= x \/ y by A52;
A57: dom g = ((F \ {x}) \ {y}) \/ {(x \/ y)} by FUNCT_2:def_1;
then A58: dom (g | ((F \ {x}) \ {y})) = (((F \ {x}) \ {y}) \/ {(x \/ y)}) /\ ((F \ {x}) \ {y}) by RELAT_1:61
.= (F \ {x}) \ {y} by XBOOLE_1:21 ;
g . (x \/ y) in rng g by A55, A57, FUNCT_1:def_3;
then reconsider gxy = g . (x \/ y) as open Subset of TM by A50, TOPS_2:def_1;
set gxyA = gxy /\ A;
gxy /\ A c= gxy by XBOOLE_1:17;
then A59: gxy /\ A c= x \/ y by A56, XBOOLE_1:1;
[#] (TM | A) = A by PRE_TOPC:def_5;
then reconsider GxyA = gxy /\ A as Subset of (TM | A) by XBOOLE_1:17;
A60: (TM | A) | GxyA = TM | (gxy /\ A) by METRIZTS:9;
then A61: gxy /\ A is finite-ind by A6, TOPDIM_1:18;
then A62: ind (gxy /\ A) = ind (TM | (gxy /\ A)) by TOPDIM_1:17;
ind GxyA <= ind (TM | A) by A6, TOPDIM_1:19;
then ind GxyA <= 0 by A6, A7, TOPDIM_1:17;
then ind (gxy /\ A) <= 0 by A61, TOPDIM_1:21;
then consider V1, V2 being open Subset of TM such that
A63: ( V1 c= x & V2 c= y ) and
A64: V1 misses V2 and
A65: gxy /\ A c= V1 \/ V2 by A5, A59, A60, A61, A62, Lm10;
reconsider gV1 = gxy /\ V1, gV2 = gxy /\ V2 as open Subset of TM ;
set h = (x,y) --> (gV1,gV2);
A66: dom ((x,y) --> (gV1,gV2)) = {x,y} by FUNCT_4:62;
then A67: dom ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = ((F \ {x}) \ {y}) \/ {x,y} by A58, FUNCT_4:def_1;
not x in F \ {x} by ZFMISC_1:56;
then A68: not x in (F \ {x}) \ {y} by ZFMISC_1:56;
A69: x in {x,y} by TARSKI:def_2;
A70: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1
.= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4
.= F by A18, A19, ZFMISC_1:116 ;
for A being Subset of TM st A in {gV1,gV2} holds
A is open by TARSKI:def_2;
then A71: {gV1,gV2} is open by TOPS_2:def_1;
A72: y in {x,y} by TARSKI:def_2;
not y in (F \ {x}) \ {y} by ZFMISC_1:56;
then A73: (F \ {x}) \ {y} misses {x,y} by A68, ZFMISC_1:51;
then A74: rng ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = (rng (g | ((F \ {x}) \ {y}))) \/ (rng ((x,y) --> (gV1,gV2))) by A58, A66, NECKLACE:6;
then reconsider gh = (g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2)) as Function of F,(bool the carrier of TM) by A67, A70, FUNCT_2:2;
A75: (F \ {x}) \ {y} c= dom gh by A67, XBOOLE_1:7;
take gh ; ::_thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds
gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b ) )
A76: x <> y by A18, ZFMISC_1:56;
then rng ((x,y) --> (gV1,gV2)) = {gV1,gV2} by FUNCT_4:64;
hence rng gh is open by A54, A71, A74, TOPS_2:13; ::_thesis: ( rng gh is Cover of A & ( for a being set st a in F holds
gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b ) )
((x,y) --> (gV1,gV2)) . x = gV1 by A76, FUNCT_4:63;
then A77: gh . x = gV1 by A66, A69, FUNCT_4:13;
((x,y) --> (gV1,gV2)) . y = gV2 by FUNCT_4:63;
then A78: gh . y = gV2 by A66, A72, FUNCT_4:13;
A79: for a, b being set st a in (F \ {x}) \ {y} & b in {x,y} & a <> b holds
gh . a misses gh . b
proof
x \/ y in {(x \/ y)} by TARSKI:def_1;
then A80: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def_3;
let a, b be set ; ::_thesis: ( a in (F \ {x}) \ {y} & b in {x,y} & a <> b implies gh . a misses gh . b )
assume that
A81: a in (F \ {x}) \ {y} and
A82: b in {x,y} and
a <> b ; ::_thesis: gh . a misses gh . b
( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A81, FUNCT_1:47, XBOOLE_0:3;
then A83: gh . a = g . a by FUNCT_4:11;
A84: a <> x \/ y
proof
assume a = x \/ y ; ::_thesis: contradiction
then A85: union F = union ((F \ {x}) \ {y}) by A49, A81, XBOOLE_1:12, ZFMISC_1:74;
not A c= union ((F \ {x}) \ {y}) by A46, SETFAM_1:def_11;
hence contradiction by A9, A85, SETFAM_1:def_11; ::_thesis: verum
end;
assume gh . a meets gh . b ; ::_thesis: contradiction
then consider z being set such that
A86: z in gh . a and
A87: z in gh . b by XBOOLE_0:3;
( z in gV1 or z in gV2 ) by A78, A77, A82, A87, TARSKI:def_2;
then z in gxy by XBOOLE_0:def_4;
then g . (x \/ y) meets g . a by A83, A86, XBOOLE_0:3;
hence contradiction by A53, A58, A80, A81, A84; ::_thesis: verum
end;
A88: {x,y} c= dom gh by A67, XBOOLE_1:7;
then A89: gh . y in rng gh by A72, FUNCT_1:def_3;
A90: gh . x in rng gh by A69, A88, FUNCT_1:def_3;
A c= union (rng gh)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A or z in union (rng gh) )
assume A91: z in A ; ::_thesis: z in union (rng gh)
A c= union (rng g) by A51, SETFAM_1:def_11;
then consider G being set such that
A92: z in G and
A93: G in rng g by A91, TARSKI:def_4;
consider Gx being set such that
A94: Gx in ((F \ {x}) \ {y}) \/ {(x \/ y)} and
A95: g . Gx = G by A57, A93, FUNCT_1:def_3;
percases ( Gx in (F \ {x}) \ {y} or Gx in {(x \/ y)} ) by A94, XBOOLE_0:def_3;
supposeA96: Gx in (F \ {x}) \ {y} ; ::_thesis: z in union (rng gh)
then ( (g | ((F \ {x}) \ {y})) . Gx = G & not Gx in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A95, FUNCT_1:47, XBOOLE_0:3;
then A97: gh . Gx = G by FUNCT_4:11;
gh . Gx in rng gh by A75, A96, FUNCT_1:def_3;
hence z in union (rng gh) by A92, A97, TARSKI:def_4; ::_thesis: verum
end;
suppose Gx in {(x \/ y)} ; ::_thesis: z in union (rng gh)
then A98: z in gxy by A92, A95, TARSKI:def_1;
then z in gxy /\ A by A91, XBOOLE_0:def_4;
then ( z in V1 or z in V2 ) by A65, XBOOLE_0:def_3;
then ( z in gV1 or z in gV2 ) by A98, XBOOLE_0:def_4;
hence z in union (rng gh) by A78, A77, A90, A89, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence rng gh is Cover of A by SETFAM_1:def_11; ::_thesis: ( ( for a being set st a in F holds
gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b ) )
A99: ( gV1 c= V1 & gV2 c= V2 ) by XBOOLE_1:17;
hereby ::_thesis: for a, b being set st a in F & b in F & a <> b holds
gh . a misses gh . b
let a be set ; ::_thesis: ( a in F implies gh . b1 c= b1 )
assume A100: a in F ; ::_thesis: gh . b1 c= b1
percases ( a in (F \ {x}) \ {y} or a in {x,y} ) by A70, A100, XBOOLE_0:def_3;
supposeA101: a in (F \ {x}) \ {y} ; ::_thesis: gh . b1 c= b1
then A102: (g | ((F \ {x}) \ {y})) . a = g . a by A58, FUNCT_1:47;
( not a in dom ((x,y) --> (gV1,gV2)) & g . a c= a ) by A52, A58, A73, A101, XBOOLE_0:3;
hence gh . a c= a by A102, FUNCT_4:11; ::_thesis: verum
end;
suppose a in {x,y} ; ::_thesis: gh . b1 c= b1
then ( a = x or a = y ) by TARSKI:def_2;
hence gh . a c= a by A63, A78, A77, A99, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
let a, b be set ; ::_thesis: ( a in F & b in F & a <> b implies gh . a misses gh . b )
assume that
A103: ( a in F & b in F ) and
A104: a <> b ; ::_thesis: gh . a misses gh . b
percases ( ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) or ( a in (F \ {x}) \ {y} & b in {x,y} ) or ( a in {x,y} & b in (F \ {x}) \ {y} ) or ( a in {x,y} & b in {x,y} ) ) by A70, A103, XBOOLE_0:def_3;
supposeA105: ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) ; ::_thesis: gh . a misses gh . b
then ( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, FUNCT_1:47, XBOOLE_0:3;
then A106: gh . a = g . a by FUNCT_4:11;
A107: ( (g | ((F \ {x}) \ {y})) . b = g . b & not b in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A105, FUNCT_1:47, XBOOLE_0:3;
g . a misses g . b by A53, A58, A104, A105;
hence gh . a misses gh . b by A106, A107, FUNCT_4:11; ::_thesis: verum
end;
suppose ( ( a in (F \ {x}) \ {y} & b in {x,y} ) or ( a in {x,y} & b in (F \ {x}) \ {y} ) ) ; ::_thesis: gh . a misses gh . b
hence gh . a misses gh . b by A79, A104; ::_thesis: verum
end;
supposeA108: ( a in {x,y} & b in {x,y} ) ; ::_thesis: gh . a misses gh . b
then ( a = x or a = y ) by TARSKI:def_2;
then ( ( a = x & b = y ) or ( a = y & b = x ) ) by A104, A108, TARSKI:def_2;
hence gh . a misses gh . b by A64, A78, A77, A99, XBOOLE_1:64; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
A109: S1[ 0 ]
proof
let A be Subset of TM; ::_thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) )
assume that
TM | A is second-countable and
A is finite-ind and
ind A <= 0 ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of A & card F <= 0 implies ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) )
assume that
F is open and
A110: F is Cover of A and
A111: card F <= 0 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
( rng {} c= bool the carrier of TM & dom {} = F ) by A111, XBOOLE_1:2;
then reconsider g = {} as Function of F,(bool the carrier of TM) by FUNCT_2:2;
take g ; ::_thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
F = {} by A111;
hence ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A110; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A109, A3);
then S1[ card F] ;
hence ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A1, A2, TOPDIM_1:18; ::_thesis: verum
end;
theorem :: TOPDIM_2:23
for n being Nat
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds
for F being finite Subset-Family of TM st F is open & F is Cover of TM holds
ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )
proof
let n be Nat; ::_thesis: for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds
for F being finite Subset-Family of TM st F is open & F is Cover of TM holds
ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )
let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= n implies for F being finite Subset-Family of TM st F is open & F is Cover of TM holds
ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) )
assume that
A1: ( TM is second-countable & TM is finite-ind ) and
A2: ind TM <= n ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of TM holds
ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )
reconsider I = n as Integer ;
consider G being finite Subset-Family of TM such that
A3: G is Cover of TM and
A4: ( G is finite-ind & ind G <= 0 ) and
A5: card G <= I + 1 and
for a, b being Subset of TM st a in G & b in G & a meets b holds
a = b by A1, A2, Th7;
set cTM = the carrier of TM;
let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of TM implies ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) )
assume that
A6: F is open and
A7: F is Cover of TM ; ::_thesis: ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )
card ((n + 1) * (card F)) = card (card ((n + 1) * (card F))) ;
then A8: card ((n + 1) * (card F)) = (n + 1) * (card F) by CARD_1:40;
defpred S1[ set , set ] means for A being Subset of TM st A = $1 holds
ex g being Function of F,(bool the carrier of TM) st
( $2 = rng g & rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) );
A9: for x being set st x in G holds
ex y being set st
( y in bool (bool the carrier of TM) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in G implies ex y being set st
( y in bool (bool the carrier of TM) & S1[x,y] ) )
assume A10: x in G ; ::_thesis: ex y being set st
( y in bool (bool the carrier of TM) & S1[x,y] )
then reconsider A = x as Subset of TM ;
A11: TM | A is second-countable by A1;
[#] TM c= union F by A7, SETFAM_1:def_11;
then A c= union F by XBOOLE_1:1;
then A12: F is Cover of A by SETFAM_1:def_11;
( A is finite-ind & ind A <= 0 ) by A4, A10, TOPDIM_1:11;
then consider g being Function of F,(bool the carrier of TM) such that
A13: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A6, A11, A12, Th22;
take rng g ; ::_thesis: ( rng g in bool (bool the carrier of TM) & S1[x, rng g] )
thus ( rng g in bool (bool the carrier of TM) & S1[x, rng g] ) by A13; ::_thesis: verum
end;
consider GG being Function of G,(bool (bool the carrier of TM)) such that
A14: for x being set st x in G holds
S1[x,GG . x] from FUNCT_2:sch_1(A9);
union (rng GG) c= union (bool (bool the carrier of TM)) by ZFMISC_1:77;
then reconsider Ugg = Union GG as Subset-Family of TM ;
A15: dom GG = G by FUNCT_2:def_1;
A16: for x being set st x in dom GG holds
card (GG . x) c= card F
proof
let x be set ; ::_thesis: ( x in dom GG implies card (GG . x) c= card F )
assume A17: x in dom GG ; ::_thesis: card (GG . x) c= card F
then reconsider A = x as Subset of TM by A15;
consider g being Function of F,(bool the carrier of TM) such that
A18: GG . x = rng g and
rng g is open and
rng g is Cover of A and
for a being set st a in F holds
g . a c= a and
for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14, A17;
dom g = F by FUNCT_2:def_1;
hence card (GG . x) c= card F by A18, CARD_1:12; ::_thesis: verum
end;
card (dom GG) c= n + 1 by A5, A15, NAT_1:39;
then A19: card Ugg c= (n + 1) *` (card F) by A16, CARD_2:86;
card (card (n + 1)) = card (n + 1) ;
then ( card (card F) = card F & card (n + 1) = n + 1 ) by CARD_1:40;
then A20: (n + 1) *` (card F) = (n + 1) * (card F) by A8, CARD_2:39;
then reconsider Ugg = Ugg as finite Subset-Family of TM by A19;
take Ugg ; ::_thesis: ( Ugg is open & Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )
thus Ugg is open ::_thesis: ( Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )
proof
let A be Subset of TM; :: according to TOPS_2:def_1 ::_thesis: ( not A in Ugg or A is open )
assume A in Ugg ; ::_thesis: A is open
then consider Y being set such that
A21: A in Y and
A22: Y in rng GG by TARSKI:def_4;
consider x being set such that
A23: ( x in dom GG & Y = GG . x ) by A22, FUNCT_1:def_3;
ex g being Function of F,(bool the carrier of TM) st
( Y = rng g & rng g is open & rng g is Cover of x & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A14, A15, A23;
hence A is open by A21, TOPS_2:def_1; ::_thesis: verum
end;
[#] TM c= union Ugg
proof
A24: [#] TM c= union G by A3, SETFAM_1:def_11;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] TM or x in union Ugg )
assume A25: x in [#] TM ; ::_thesis: x in union Ugg
consider A being set such that
A26: x in A and
A27: A in G by A24, A25, TARSKI:def_4;
consider g being Function of F,(bool the carrier of TM) such that
A28: GG . A = rng g and
rng g is open and
A29: rng g is Cover of A and
for a being set st a in F holds
g . a c= a and
for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14, A27;
A c= union (rng g) by A29, SETFAM_1:def_11;
then consider y being set such that
A30: x in y and
A31: y in rng g by A26, TARSKI:def_4;
GG . A in rng GG by A15, A27, FUNCT_1:def_3;
then y in Ugg by A28, A31, TARSKI:def_4;
hence x in union Ugg by A30, TARSKI:def_4; ::_thesis: verum
end;
hence Ugg is Cover of TM by SETFAM_1:def_11; ::_thesis: ( Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )
thus Ugg is_finer_than F ::_thesis: ( card Ugg <= (card F) * (n + 1) & order Ugg <= n )
proof
let A be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not A in Ugg or ex b1 being set st
( b1 in F & A c= b1 ) )
assume A in Ugg ; ::_thesis: ex b1 being set st
( b1 in F & A c= b1 )
then consider Y being set such that
A32: A in Y and
A33: Y in rng GG by TARSKI:def_4;
consider x being set such that
A34: ( x in dom GG & Y = GG . x ) by A33, FUNCT_1:def_3;
consider g being Function of F,(bool the carrier of TM) such that
A35: Y = rng g and
rng g is open and
rng g is Cover of x and
A36: for a being set st a in F holds
g . a c= a and
for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14, A15, A34;
dom g = F by FUNCT_2:def_1;
then ex z being set st
( z in F & g . z = A ) by A32, A35, FUNCT_1:def_3;
hence ex b1 being set st
( b1 in F & A c= b1 ) by A36; ::_thesis: verum
end;
thus card Ugg <= (card F) * (n + 1) by A19, A20, NAT_1:39; ::_thesis: order Ugg <= n
defpred S2[ set , set ] means $1 in GG . $2;
now__::_thesis:_for_H_being_finite_Subset-Family_of_TM_st_H_c=_Ugg_&_card_H_>_n_+_1_holds_
meet_H_is_empty
let H be finite Subset-Family of TM; ::_thesis: ( H c= Ugg & card H > n + 1 implies meet H is empty )
assume that
A37: H c= Ugg and
A38: card H > n + 1 ; ::_thesis: meet H is empty
not H is empty by A38;
then consider XX being set such that
A39: XX in H by XBOOLE_0:def_1;
A40: for x being set st x in H holds
ex y being set st
( y in G & S2[x,y] )
proof
let A be set ; ::_thesis: ( A in H implies ex y being set st
( y in G & S2[A,y] ) )
assume A in H ; ::_thesis: ex y being set st
( y in G & S2[A,y] )
then consider Y being set such that
A41: A in Y and
A42: Y in rng GG by A37, TARSKI:def_4;
ex x being set st
( x in dom GG & Y = GG . x ) by A42, FUNCT_1:def_3;
hence ex y being set st
( y in G & S2[A,y] ) by A41; ::_thesis: verum
end;
consider q being Function of H,G such that
A43: for x being set st x in H holds
S2[x,q . x] from FUNCT_2:sch_1(A40);
ex y being set st
( y in G & S2[XX,y] ) by A40, A39;
then A44: dom q = H by FUNCT_2:def_1;
assume not meet H is empty ; ::_thesis: contradiction
then consider x being set such that
A45: x in meet H by XBOOLE_0:def_1;
for x1, x2 being set st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 implies x1 = x2 )
assume that
A46: x1 in dom q and
A47: x2 in dom q and
A48: q . x1 = q . x2 ; ::_thesis: x1 = x2
( x in x1 & x in x2 ) by A45, A46, A47, SETFAM_1:def_1;
then A49: x1 meets x2 by XBOOLE_0:3;
q . x1 in rng q by A46, FUNCT_1:def_3;
then q . x1 in G ;
then consider g being Function of F,(bool the carrier of TM) such that
A50: GG . (q . x1) = rng g and
rng g is open and
rng g is Cover of q . x1 and
for a being set st a in F holds
g . a c= a and
A51: for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14;
A52: dom g = F by FUNCT_2:def_1;
x2 in GG . (q . x1) by A43, A47, A48;
then A53: ex y2 being set st
( y2 in F & x2 = g . y2 ) by A50, A52, FUNCT_1:def_3;
x1 in GG . (q . x1) by A43, A46;
then ex y1 being set st
( y1 in F & x1 = g . y1 ) by A50, A52, FUNCT_1:def_3;
hence x1 = x2 by A49, A51, A53; ::_thesis: verum
end;
then A54: q is one-to-one by FUNCT_1:def_4;
rng q c= G ;
then card H c= card G by A54, A44, CARD_1:10;
then card H <= card G by NAT_1:39;
hence contradiction by A5, A38, XXREAL_0:2; ::_thesis: verum
end;
hence order Ugg <= n by Th3; ::_thesis: verum
end;
theorem :: TOPDIM_2:24
for n being Nat
for TM being metrizable TopSpace st TM is finite-ind holds
for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
proof
let n be Nat; ::_thesis: for TM being metrizable TopSpace st TM is finite-ind holds
for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
let TM be metrizable TopSpace; ::_thesis: ( TM is finite-ind implies for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume A1: TM is finite-ind ; ::_thesis: for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
set cTM = [#] TM;
let A be Subset of TM; ::_thesis: ( ind (A `) <= n & TM | (A `) is second-countable implies for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume that
A2: ind (A `) <= n and
A3: TM | (A `) is second-countable ; ::_thesis: for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
let A1, A2 be closed Subset of TM; ::_thesis: ( A = A1 \/ A2 implies ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume A4: A = A1 \/ A2 ; ::_thesis: ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
set A12 = A1 /\ A2;
set T912 = TM | (([#] TM) \ (A1 /\ A2));
A5: [#] (TM | (([#] TM) \ (A1 /\ A2))) = ([#] TM) \ (A1 /\ A2) by PRE_TOPC:def_5;
A ` c= ([#] TM) \ (A1 /\ A2) by A4, XBOOLE_1:29, XBOOLE_1:34;
then reconsider A19 = A1 \ (A1 /\ A2), A29 = A2 \ (A1 /\ A2), A9 = A ` as Subset of (TM | (([#] TM) \ (A1 /\ A2))) by A5, XBOOLE_1:33;
A2 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) = (A2 /\ ([#] TM)) \ (A1 /\ A2) by A5, XBOOLE_1:49
.= A29 by XBOOLE_1:28 ;
then reconsider A29 = A29 as closed Subset of (TM | (([#] TM) \ (A1 /\ A2))) by PRE_TOPC:13;
A1 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) = (A1 /\ ([#] TM)) \ (A1 /\ A2) by A5, XBOOLE_1:49
.= A19 by XBOOLE_1:28 ;
then reconsider A19 = A19 as closed Subset of (TM | (([#] TM) \ (A1 /\ A2))) by PRE_TOPC:13;
A1 \ A2 = A19 by XBOOLE_1:47;
then A19 misses A2 by XBOOLE_1:79;
then A6: A19 misses A29 by XBOOLE_1:36, XBOOLE_1:63;
A7: ind (A `) = ind A9 by A1, TOPDIM_1:21;
(TM | (([#] TM) \ (A1 /\ A2))) | A9 is second-countable by A3, METRIZTS:9;
then consider L being Subset of (TM | (([#] TM) \ (A1 /\ A2))) such that
A8: L separates A19,A29 and
A9: ind (L /\ A9) <= n - 1 by A1, A2, A6, A7, Th11;
consider U, W being open Subset of (TM | (([#] TM) \ (A1 /\ A2))) such that
A10: A19 c= U and
A11: A29 c= W and
A12: U misses W and
A13: L = (U \/ W) ` by A8, METRIZTS:def_3;
[#] (TM | (([#] TM) \ (A1 /\ A2))) c= [#] TM by PRE_TOPC:def_4;
then reconsider L9 = L, U9 = U, W9 = W as Subset of TM by XBOOLE_1:1;
A14: ( A1 = (A1 \ (A1 /\ A2)) \/ (A1 /\ A2) & A2 = (A2 \ (A1 /\ A2)) \/ (A1 /\ A2) ) by XBOOLE_1:17, XBOOLE_1:45;
L misses A
proof
assume L meets A ; ::_thesis: contradiction
then consider x being set such that
A15: x in L and
A16: x in A by XBOOLE_0:3;
A17: ( x in A1 or x in A2 ) by A4, A16, XBOOLE_0:def_3;
not x in A1 /\ A2 by A5, A15, XBOOLE_0:def_5;
then ( x in A19 or x in A29 ) by A17, XBOOLE_0:def_5;
then x in U \/ W by A10, A11, XBOOLE_0:def_3;
hence contradiction by A13, A15, XBOOLE_0:def_5; ::_thesis: verum
end;
then A18: L = L9 \ A by XBOOLE_1:83
.= (L /\ ([#] TM)) \ A by XBOOLE_1:28
.= L /\ A9 by XBOOLE_1:49 ;
A19: ([#] TM) \ (([#] TM) \ (A1 /\ A2)) = ([#] TM) /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:28 ;
A20: A1 \ (A1 \ (A1 /\ A2)) = A1 /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:17, XBOOLE_1:28 ;
(A1 /\ A2) ` is open ;
then reconsider U9 = U9, W9 = W9 as open Subset of TM by A5, TSEP_1:9;
take X2 = W9 ` ; ::_thesis: ex X2 being closed Subset of TM st
( [#] TM = X2 \/ X2 & A1 c= X2 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X2) \ (A1 /\ A2)) <= n - 1 )
take X1 = U9 ` ; ::_thesis: ( [#] TM = X2 \/ X1 & A1 c= X2 & A2 c= X1 & A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A21: W9 c= X1 by A12, SUBSET_1:23;
A22: W \/ (([#] TM) \ (U \/ W)) = W \/ (X1 /\ X2) by XBOOLE_1:53
.= (W9 \/ X1) /\ (W \/ X2) by XBOOLE_1:24
.= (W9 \/ X1) /\ ([#] TM) by XBOOLE_1:45
.= X1 /\ ([#] TM) by A21, XBOOLE_1:12
.= X1 by XBOOLE_1:28 ;
thus X2 \/ X1 = ([#] TM) \ (U9 /\ W9) by XBOOLE_1:54
.= ([#] TM) \ {} by A12, XBOOLE_0:def_7
.= [#] TM ; ::_thesis: ( A1 c= X2 & A2 c= X1 & A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A23: U9 c= X2 by A12, SUBSET_1:23;
A24: U \/ (([#] TM) \ (U \/ W)) = U \/ (X1 /\ X2) by XBOOLE_1:53
.= (U9 \/ X1) /\ (U \/ X2) by XBOOLE_1:24
.= ([#] TM) /\ (U \/ X2) by XBOOLE_1:45
.= ([#] TM) /\ X2 by A23, XBOOLE_1:12
.= X2 by XBOOLE_1:28 ;
([#] TM) \ (([#] TM) \ (A1 /\ A2)) c= ([#] TM) \ (U \/ W) by A5, XBOOLE_1:34;
hence A25: ( A1 c= X2 & A2 c= X1 ) by A10, A11, A14, A19, A24, A22, XBOOLE_1:13; ::_thesis: ( A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
then A26: A1 /\ A2 c= A1 /\ X1 by XBOOLE_1:26;
A1 /\ X1 = (([#] TM) /\ A1) \ U9 by XBOOLE_1:49
.= A1 \ U9 by XBOOLE_1:28 ;
then A1 /\ X1 c= A1 /\ A2 by A10, A20, XBOOLE_1:34;
hence A1 /\ X1 = A1 /\ A2 by A26, XBOOLE_0:def_10; ::_thesis: ( A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A27: A2 \ (A2 \ (A1 /\ A2)) = A2 /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:17, XBOOLE_1:28 ;
A28: A1 /\ A2 c= A2 /\ X2 by A25, XBOOLE_1:26;
A2 /\ X2 = (([#] TM) /\ A2) \ W9 by XBOOLE_1:49
.= A2 \ W9 by XBOOLE_1:28 ;
then A2 /\ X2 c= A1 /\ A2 by A11, A27, XBOOLE_1:34;
hence A1 /\ A2 = X2 /\ A2 by A28, XBOOLE_0:def_10; ::_thesis: ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1
(X2 /\ X1) \ (A1 /\ A2) = (([#] TM) \ (W9 \/ U9)) \ (A1 /\ A2) by XBOOLE_1:53
.= ([#] TM) \ ((W9 \/ U9) \/ (A1 /\ A2)) by XBOOLE_1:41
.= L by A5, A13, XBOOLE_1:41 ;
hence ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 by A1, A9, A18, TOPDIM_1:21; ::_thesis: verum
end;