:: Small {I}nductive {D}imension of {T}opological {S}paces
:: by Karol P\c{a}k
::
:: Received June 29, 2009
:: Copyright (c) 2009-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, SUBSET_1, RELAT_1, SETFAM_1, RCOMP_1, NAT_1,
INT_1, XBOOLE_0, TOPS_1, TARSKI, PROB_1, ZFMISC_1, STRUCT_0, FUNCT_1,
CARD_1, ARYTM_3, PARTFUN1, FINSET_1, XXREAL_0, COMPTS_1, ARYTM_1,
ORDINAL1, T_0TOPSP, TOPS_2, CARD_5, METRIZTS, RLVECT_3, CARD_3, MCART_1,
PCOMPS_1, WAYBEL23, TOPDIM_1, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, ORDINAL1,
XTUPLE_0, MCART_1, FUNCT_2, CARD_1, CARD_3, CANTOR_1, FINSET_1, NUMBERS,
ZFMISC_1, XXREAL_0, XCMPLX_0, REAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC,
TOPS_1, TOPS_2, INT_1, NAT_1, STRUCT_0, COMPTS_1, PCOMPS_1, PROB_1,
WAYBEL23, BORSUK_1, BORSUK_3, METRIZTS;
constructors TOPS_1, TOPS_2, BORSUK_1, REAL_1, CANTOR_1, WAYBEL23, COMPTS_1,
BORSUK_3, METRIZTS, PCOMPS_1, KURATO_0, EUCLID, XTUPLE_0;
registrations BORSUK_3, CARD_1, COMPTS_1, FINSET_1, FUNCT_2, INT_1, NAT_1,
ORDINAL1, PRE_TOPC, STRUCT_0, SUBSET_1, TOPREAL6, TOPS_1, XCMPLX_0,
XREAL_0, XXREAL_0, YELLOW13, METRIZTS, RELSET_1, BORSUK_1, XTUPLE_0;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TOPS_2, TARSKI, XBOOLE_0;
equalities COMPTS_1, STRUCT_0, SUBSET_1, TOPS_1, XBOOLE_0, CARD_1, ORDINAL1;
expansions TOPS_2, TARSKI, XBOOLE_0, FUNCT_2;
theorems CARD_2, CARD_3, FUNCT_1, FUNCT_2, INT_1, ORDINAL1, MCART_1, NAT_1,
PRE_TOPC, PROB_1, RELAT_1, SETFAM_1, SETLIM_1, SUBSET_1, TARSKI,
TOPGEN_1, TOPGRP_1, TOPS_1, TOPS_2, TOPS_3, TSEP_1, TSP_1, T_0TOPSP,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, YELLOW12, YELLOW_9, ZFMISC_1,
METRIZTS, KURATO_0, XTUPLE_0;
schemes CLASSES1, FRAENKEL, FUNCT_2, NAT_1, SUBSET_1;
begin :: Preliminaries
reserve T,T1,T2 for TopSpace,
A,B for Subset of T,
F for Subset of T|A,
G,G1, G2 for Subset-Family of T,
U,W for open Subset of T|A,
p for Point of T|A,
n for Nat,
I for Integer;
theorem Th1:
F = B/\A implies Fr F c= Fr B/\A
proof
A1: [#](T|A)=A by PRE_TOPC:def 5;
[#](T|A)c=[#]T by PRE_TOPC:def 4;
then reconsider F9=F,Fd=F` as Subset of T by XBOOLE_1:1;
assume
A2: F=B/\A;
then Cl F9 c=Cl B by PRE_TOPC:19,XBOOLE_1:18;
then Cl F9/\A c=Cl B/\A by XBOOLE_1:26;
then
A3: Cl F c=Cl B/\A by A1,PRE_TOPC:17;
[#](T|A)=A by PRE_TOPC:def 5;
then F`=A\B by A2,XBOOLE_1:47;
then F`c=B` by XBOOLE_1:35;
then Cl Fd c=Cl B` by PRE_TOPC:19;
then
A4: Cl Fd/\A c=Cl B`/\A by XBOOLE_1:26;
Cl F`=Cl Fd/\[#](T|A) by PRE_TOPC:17;
then Cl F`c=Cl B` by A1,A4,XBOOLE_1:18;
then Cl F/\Cl F`c=(Cl B/\A)/\Cl B` by A3,XBOOLE_1:27;
hence thesis by XBOOLE_1:16;
end;
theorem Th2:
T is normal iff for A,B be closed Subset of T st A misses B ex U,
W be open Subset of T st A c=U & B c=W & Cl U misses Cl W
proof
hereby
assume
A1: T is normal;
let A1,A2 be closed Subset of T;
assume A1 misses A2;
then consider B1,B2 be Subset of T such that
A2: B1 is open and
A3: B2 is open and
A4: A1 c=B1 and
A5: A2 c=B2 and
A6: B1 misses B2 by A1,PRE_TOPC:def 12;
A1 misses B1` by A4,SUBSET_1:24;
then consider C1,C2 be Subset of T such that
A7: C1 is open and
A8: C2 is open and
A9: A1 c=C1 and
A10: B1`c=C2 and
A11: C1 misses C2 by A1,A2,PRE_TOPC:def 12;
A12: Cl C2`=C2` & C2`c=B1 by A8,A10,PRE_TOPC:22,SUBSET_1:17;
A2 misses B2` by A5,SUBSET_1:24;
then consider D1,D2 be Subset of T such that
A13: D1 is open and
A14: D2 is open and
A15: A2 c=D1 and
A16: B2`c=D2 and
A17: D1 misses D2 by A1,A3,PRE_TOPC:def 12;
reconsider C1,D1 as open Subset of T by A13,A7;
take C1,D1;
D1 c=D2` by A17,SUBSET_1:23;
then
A18: Cl D1 c=Cl D2` by PRE_TOPC:19;
C1 c=C2` by A11,SUBSET_1:23;
then Cl C1 c=Cl C2` by PRE_TOPC:19;
then
A19: Cl C1 c=B1 by A12;
Cl D2`=D2` & D2`c=B2 by A14,A16,PRE_TOPC:22,SUBSET_1:17;
then Cl D1 c=B2 by A18;
hence A1 c=C1 & A2 c=D1 & Cl C1 misses Cl D1 by A6,A15,A9,A19,XBOOLE_1:64;
end;
assume
A20: for A,B be closed Subset of T st A misses B ex U,W be open Subset
of T st A c=U & B c=W & Cl U misses Cl W;
for A,B be Subset of T st A is closed & B is closed & A misses B ex U,W
be Subset of T st U is open & W is open & A c=U & B c=W & U misses W
proof
let A,B be Subset of T;
assume A is closed & B is closed & A misses B;
then consider U,W be open Subset of T such that
A21: A c=U & B c=W & Cl U misses Cl W by A20;
take U,W;
U c=Cl U & W c=Cl W by PRE_TOPC:18;
hence thesis by A21,XBOOLE_1:64;
end;
hence thesis by PRE_TOPC:def 12;
end;
:: The sequence of a subset family of topological spaces
:: with limited small inductive dimension
definition
let T;
func Seq_of_ind T -> SetSequence of ((bool the carrier of T) qua set)
means
:Def1:
it.0
= { {}T } & ( A in it.(n+1) iff A in it.n or for p,U st p in U ex W st p in W &
W c=U & Fr W in it.n);
existence
proof
defpred P[object,object] means
ex D1,D2 being set st D1= $1 & D2 = $2 &
for A holds A in D2 iff A in D1 or for p,U st p in U ex W st
p in W & W c=U & Fr W in D1;
set C = the carrier of T;
reconsider E={{}T} as Element of bool bool C;
A1: for x be object st x in bool bool C
ex y be object st y in bool bool C & P[x ,y]
proof
let x be object such that
x in bool bool C;
reconsider xx = x as set by TARSKI:1;
defpred Q[object] means
for A st A=$1 holds A in xx or for p,U st p in U ex
W st p in W & W c=U & Fr W in xx;
consider y be Subset of bool C such that
A2: for z be set holds z in y iff z in bool C & Q[z] from SUBSET_1:
sch 1;
take y;
thus y in bool bool C;
reconsider yy = y as set;
take xx,yy;
thus xx = x & yy = y;
let A;
A in y iff Q[A] by A2;
hence thesis;
end;
consider p be Function of bool bool C,bool bool C such that
A3: for x be object st x in bool bool C holds P[x,p.x] from FUNCT_2:sch 1
(A1);
deffunc F(set,set)=p/.$2;
consider f be sequence of bool bool C such that
A4: f.0=E and
A5: for n holds f.(n+1)=F(n,f.n) from NAT_1:sch 12;
reconsider f as SetSequence of ((bool the carrier of T) qua set);
take f;
now
let n;
A6: f.(n+1)=p/.(f.n) by A5
.=p.(f.n);
P[f.n,p.(f.n)] by A3;
hence A in f.(n+1) iff A in f.n or for p,U st p in U ex W st p in W & W
c=U & Fr W in f.n by A6;
end;
hence thesis by A4;
end;
uniqueness
proof
let Ind1,Ind2 be SetSequence of bool (the carrier of T) qua set
such that
A7: Ind1.0={{}T} & (A in Ind1.(n+1) iff A in Ind1.n or for p,U st p in
U ex W st p in W & W c=U & Fr W in Ind1.n) and
A8: Ind2.0={{}T} & (A in Ind2.(n+1) iff A in Ind2.n or for p,U st p
in U ex W st p in W & W c=U & Fr W in Ind2.n);
defpred P[Nat] means Ind1.$1=Ind2.$1;
A9: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A10: P[n];
thus Ind1.(n+1)c=Ind2.(n+1)
proof
let x be object such that
A11: x in Ind1.(n+1);
reconsider A=x as Subset of T by A11;
A in Ind1.n or for p be Point of T|A,U be open Subset of T|A st p
in U ex W be open Subset of T|A st p in W & W c=U & Fr W in Ind1.n by A7,A11;
hence thesis by A8,A10;
end;
let x be object such that
A12: x in Ind2.(n+1);
reconsider A=x as Subset of T by A12;
A in Ind2.n or for p be Point of T|A,U be open Subset of T|A st p
in U ex W be open Subset of T|A st p in W & W c=U & Fr W in Ind2.n by A8,A12;
hence thesis by A7,A10;
end;
A13: P[0] by A7,A8;
for n be Nat holds P[n] from NAT_1:sch 2(A13,A9);
hence thesis;
end;
end;
registration
let T;
cluster Seq_of_ind T -> non-descending;
coherence
proof
for n be Nat holds (Seq_of_ind T).n c=(Seq_of_ind T).(n+1) by Def1;
hence thesis by KURATO_0:def 4;
end;
end;
theorem Th3:
for F st F = B holds F in (Seq_of_ind T|A).n iff B in (Seq_of_ind T).n
proof
defpred P[Nat] means for F be Subset of T|A,B st F=B holds F in (Seq_of_ind
T|A).$1 iff B in (Seq_of_ind T).$1;
A1: for n st P[n] holds P[n+1]
proof
set TA=T|A;
let n such that
A2: P[n];
set n1=n+1;
let F be Subset of TA,B such that
A3: F=B;
set TAF=(T|A)|F;
set TB=T|B;
A4: TAF=TB by A3,METRIZTS:9;
A5: [#]TB c=[#]T by PRE_TOPC:def 4;
hereby
assume
A6: F in (Seq_of_ind TA).n1;
per cases by A6,Def1;
suppose
F in (Seq_of_ind TA).n;
then B in (Seq_of_ind T).n by A2,A3;
hence B in (Seq_of_ind T).n1 by Def1;
end;
suppose
A7: for p be Point of TAF,U be open Subset of TAF st p in U ex W
be open Subset of TAF st p in W & W c=U & Fr W in (Seq_of_ind TA).n;
now
let p be Point of TB,U be open Subset of TB such that
A8: p in U;
reconsider U9=U as open Subset of TAF by A4;
consider W9 be open Subset of TAF such that
A9: p in W9 & W9 c=U9 & Fr W9 in (Seq_of_ind TA).n by A7,A8;
reconsider W=W9 as open Subset of TB by A4;
take W;
Fr W is Subset of T by A5,XBOOLE_1:1;
hence p in W & W c=U & Fr W in (Seq_of_ind T).n by A2,A4,A9;
end;
hence B in (Seq_of_ind T).n1 by Def1;
end;
end;
A10: [#]TAF c=[#]TA by PRE_TOPC:def 4;
assume
A11: B in (Seq_of_ind T).n1;
per cases by A11,Def1;
suppose
B in (Seq_of_ind T).n;
then F in (Seq_of_ind TA).n by A2,A3;
hence F in (Seq_of_ind TA).n1 by Def1;
end;
suppose
A12: for p be Point of TB,U be open Subset of TB st p in U ex W be
open Subset of TB st p in W & W c=U & Fr W in (Seq_of_ind T).n;
now
let p be Point of TAF,U be open Subset of TAF such that
A13: p in U;
reconsider U9=U as open Subset of TB by A4;
consider W9 be open Subset of TB such that
A14: p in W9 & W9 c=U9 & Fr W9 in (Seq_of_ind T).n by A12,A13;
reconsider W=W9 as open Subset of TAF by A4;
take W;
Fr W is Subset of TA by A10,XBOOLE_1:1;
hence p in W & W c=U & Fr W in (Seq_of_ind TA).n by A2,A4,A14;
end;
hence F in (Seq_of_ind TA).n1 by Def1;
end;
end;
A15: P[0]
proof
A16: (Seq_of_ind T|A).0={{}(T|A)} by Def1
.={{}T}
.=(Seq_of_ind T).0 by Def1;
let F be Subset of T|A,B;
assume F=B;
hence thesis by A16;
end;
for n holds P[n] from NAT_1:sch 2(A15,A1);
hence thesis;
end;
definition
let T,A;
attr A is with_finite_small_inductive_dimension means
:Def2:
ex n st A in ( Seq_of_ind T).n;
end;
notation
let T,A;
synonym A is finite-ind for A is with_finite_small_inductive_dimension;
end;
definition
let T,G;
attr G is with_finite_small_inductive_dimension means
ex n st G c=( Seq_of_ind T).n;
end;
notation
let T,G;
synonym G is finite-ind for G is with_finite_small_inductive_dimension;
end;
theorem
A in G & G is finite-ind implies A is finite-ind;
Lm1: for T be TopSpace,A be finite Subset of T holds A is finite-ind & A in (
Seq_of_ind T).card A
proof
defpred P[Nat] means for T be TopSpace,A be finite Subset of T st card A<=$1
holds A is finite-ind & A in (Seq_of_ind T).card A;
let T be TopSpace,A be finite Subset of T;
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
let T be TopSpace,A be finite Subset of T such that
A3: card A<=n+1;
per cases by A3,NAT_1:8;
suppose
card A<=n;
hence thesis by A2;
end;
suppose
A4: card A=n+1;
for p be Point of T|A,U be open Subset of T|A st p in U ex W be open
Subset of T|A st p in W & W c=U & Fr W in (Seq_of_ind T).n
proof
let p be Point of T|A,U be open Subset of T|A such that
A5: p in U;
take W=U;
{p}c=W by A5,ZFMISC_1:31;
then
A6: Fr W=Cl W\W & A\W c=A\{p} by TOPS_1:42,XBOOLE_1:34;
thus p in W & W c=U by A5;
[#](T|A)c=[#]T by PRE_TOPC:def 4;
then reconsider FrW=Fr W as Subset of T by XBOOLE_1:1;
A7: A\{p}c=A & not p in A\{p} by ZFMISC_1:56;
A8: [#](T|A)=A by PRE_TOPC:def 5;
then p in A by A5;
then
A9: A\{p}c finite-ind for Subset of T;
coherence by Lm1;
cluster empty -> finite-ind for Subset-Family of T;
coherence
proof
let G;
assume G is empty;
then
A1: G c={{}T};
(Seq_of_ind T).0={{}T} by Def1;
hence thesis by A1;
end;
cluster non empty finite-ind for Subset-Family of T;
existence
proof
(Seq_of_ind T).0={{}T} by Def1;
then {{}T} is finite-ind;
hence thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster non empty finite-ind for Subset of T;
existence
proof
consider x be object such that
A1: x in [#]T by XBOOLE_0:def 1;
{x} is Subset of T by A1,ZFMISC_1:31;
hence thesis;
end;
end;
definition
let T;
attr T is with_finite_small_inductive_dimension means
:Def4:
[#]T is with_finite_small_inductive_dimension;
end;
notation
let T;
synonym T is finite-ind for T is with_finite_small_inductive_dimension;
end;
registration
cluster empty -> finite-ind for TopSpace;
coherence;
end;
Lm2: for X be set holds X in (Seq_of_ind 1TopSp X).1
proof
let X be set;
set T=1TopSp X;
set CT=[#]T;
now
let p be Point of T|CT,U be open Subset of T|CT such that
A1: p in U;
take W=U;
A2: [#](T|CT)=CT by PRE_TOPC:def 5;
then reconsider W9=U as Subset of T;
W9` is open by PRE_TOPC:def 2;
then W9 is open & W9 is closed by PRE_TOPC:def 2,TOPS_1:3;
then Fr W9={}T by TOPGEN_1:14;
then
A3: Fr W9/\CT={};
W=W/\[#]T by A2,XBOOLE_1:28;
then Fr W c={}T by A3,Th1;
then
A4: Fr W={}T;
(Seq_of_ind T).0={{}T} by Def1;
hence p in W & W c=U & Fr W in (Seq_of_ind T).0 by A1,A4,TARSKI:def 1;
end;
then CT in (Seq_of_ind T).(0+1) by Def1;
hence thesis;
end;
registration
let X be set;
cluster 1TopSp X -> finite-ind;
coherence
proof
set T=1TopSp X;
[#]T in (Seq_of_ind 1TopSp X).1 by Lm2;
then [#]T is finite-ind;
hence thesis;
end;
end;
registration
cluster non empty finite-ind for TopSpace;
existence
proof
take 1TopSp the non empty set;
thus thesis;
end;
end;
reserve Af for finite-ind Subset of T,
Tf for finite-ind TopSpace;
begin :: Concept of the Small Inductive Dimension
definition
let T;
let A such that
A1: A is finite-ind;
func ind A -> Integer means
:Def5:
A in (Seq_of_ind T).(it+1) & not A in ( Seq_of_ind T).it;
existence
proof
defpred P[Nat] means A in (Seq_of_ind T).$1;
A2: ex n st P[n] by A1;
consider MIN be Nat such that
A3: P[MIN] and
A4: for n st P[n] holds MIN<=n from NAT_1:sch 5(A2);
take I=MIN-1;
now
assume
A5: A in (Seq_of_ind T).I;
then I in dom(Seq_of_ind T) by FUNCT_1:def 2;
then reconsider i=I as Element of NAT;
MIN<=i by A4,A5;
then MIN*I2;
then
A11: I1>=i21 by INT_1:7;
then reconsider i1=I1 as Element of NAT by INT_1:3;
(Seq_of_ind T).i21 c=(Seq_of_ind T).i1 by A11,PROB_1:def 5;
hence contradiction by A7,A8;
end;
I2<=I1
proof
assume I1=i11 by INT_1:7;
then reconsider i2=I2 as Element of NAT by INT_1:3;
(Seq_of_ind T).i11 c=(Seq_of_ind T).i2 by A12,PROB_1:def 5;
hence contradiction by A6,A9;
end;
hence thesis by A10,XXREAL_0:1;
end;
end;
theorem Th5:
-1 <= ind Af
proof
Af in (Seq_of_ind T).(1+ind Af) by Def5;
then
A1: (ind Af)+1 in dom(Seq_of_ind T) by FUNCT_1:def 2;
0=-1+1;
hence thesis by A1,XREAL_1:6;
end;
theorem Th6:
ind Af = -1 iff Af is empty
proof
not -1 in dom Seq_of_ind T;
then
A1: not Af in (Seq_of_ind T).(-1) by FUNCT_1:def 2;
A2: (Seq_of_ind T).0={{}T} by Def1;
hereby
assume ind Af=-1;
then Af in (Seq_of_ind T).(-1+1) by Def5;
hence Af is empty by A2,TARSKI:def 1;
end;
assume Af is empty;
then
A3: Af in (Seq_of_ind T).0 by A2,TARSKI:def 1;
-1+1=0;
hence thesis by A1,A3,Def5;
end;
Lm3: ind Af+1 is Nat
proof
Af in (Seq_of_ind T).(1+ind Af) by Def5;
then (ind Af)+1 in dom(Seq_of_ind T) by FUNCT_1:def 2;
hence thesis;
end;
registration
let T be non empty TopSpace;
let A be non empty finite-ind Subset of T;
cluster ind A -> natural;
coherence
proof
ind A >= -1 by Th5;
then ind A > -1 or ind A = -1 by XXREAL_0:1;
then ind A >= -1+1 by Th6,INT_1:7;
then ind A in NAT by INT_1:3;
hence thesis;
end;
end;
theorem Th7:
ind Af <= n-1 iff Af in (Seq_of_ind T).n
proof
set I=ind Af;
A1: Af in (Seq_of_ind T).(I+1) by Def5;
A2: I+1 is Nat by Lm3;
hereby
assume I<=n-1;
then
A3: I+1<=n-1+1 by XREAL_1:6;
I+1 in NAT & n in NAT by A2,ORDINAL1:def 12;
then (Seq_of_ind T).(I+1)c=(Seq_of_ind T).n by A3,PROB_1:def 5;
hence Af in (Seq_of_ind T).n by A1;
end;
assume
A4: Af in (Seq_of_ind T).n;
assume I>n-1;
then
A5: I>=n-1+1 by INT_1:7;
then n in NAT & I in NAT by INT_1:3;
then (Seq_of_ind T).n c=(Seq_of_ind T).I by A5,PROB_1:def 5;
hence contradiction by A4,Def5;
end;
theorem
for A be finite Subset of T holds ind A < card A
proof
let A be finite Subset of T;
A in (Seq_of_ind T).(card A) by Lm1;
then
A1: ind A<=card A-1 by Th7;
card A-1 Integer means
:Def6:
G c= (Seq_of_ind T).(it+1) & -1<=it & for
i be Integer st-1<=i & G c= (Seq_of_ind T).(i+1) holds it<=i;
existence
proof
defpred P[Nat] means G c=(Seq_of_ind T).$1;
A2: ex n st P[n] by A1;
consider MIN be Nat such that
A3: P[MIN] and
A4: for n st P[n] holds MIN<=n from NAT_1:sch 5(A2);
take I=MIN-1;
A5: now
let i be Integer such that
A6: -1<=i and
A7: G c=(Seq_of_ind T).(i+1);
-1+1<=i+1 by A6,XREAL_1:6;
then i+1 in NAT by INT_1:3;
then reconsider I1=i+1 as Nat;
MIN=I+1 & MIN<=I1 by A4,A7;
hence I<=i by XREAL_1:6;
end;
I>=0-1 by XREAL_1:9;
hence thesis by A3,A5;
end;
uniqueness
proof
let I1,I2 be Integer;
assume G c=(Seq_of_ind T).(I1+1) & -1<=I1 & ( for i be Integer st-1<=i &
G c=( Seq_of_ind T).(i+1) holds I1<=i)& G c=( Seq_of_ind T).(I2+1) &( -1<=I2 &
for i be Integer st-1<=i & G c=(Seq_of_ind T).(i+1) holds I2<=i );
then I2<=I1 & I1<=I2;
hence thesis by XXREAL_0:1;
end;
end;
theorem
ind G = -1 & G is finite-ind iff G c= {{}T}
proof
A1: {{}T}=(Seq_of_ind T).0 by Def1;
0=-1+1;
hence ind G=-1 & G is finite-ind implies G c={{}T} by A1,Def6;
assume
A2: G c={{}T};
then
A3: G is finite-ind by A1;
then
A4: -1<=ind G by Def6;
0=-1+1;
then ind G<=-1 by A1,A2,A3,Def6;
hence thesis by A1,A2,A4,XXREAL_0:1;
end;
theorem Th11:
G is finite-ind & ind G <= I iff -1 <= I & for A st A in G holds
A is finite-ind & ind A <= I
proof
hereby
assume that
A1: G is finite-ind and
A2: ind G<=I;
ind G>=-1 by A1,Def6;
then ind G+1>=-1+1 by XREAL_1:6;
then ind G+1 in NAT by INT_1:3;
then reconsider iG=ind G+1 as Nat;
A3: G c=(Seq_of_ind T).iG by A1,Def6;
-1<=ind G by A1,Def6;
hence -1<=I by A2,XXREAL_0:2;
let A such that
A4: A in G;
thus A is finite-ind by A1,A4;
then ind A<=iG-1 by A3,A4,Th7;
hence ind A<=I by A2,XXREAL_0:2;
end;
assume that
A5: -1<=I and
A6: for A st A in G holds A is finite-ind & ind A<=I;
-1+1<=I+1 by A5,XREAL_1:6;
then reconsider I1=I+1 as Element of NAT by INT_1:3;
A7: G c=(Seq_of_ind T).I1
proof
let x be object such that
A8: x in G;
reconsider A=x as Subset of T by A8;
A9: I=I1-1;
A is finite-ind & ind A<=I by A6,A8;
hence thesis by A9,Th7;
end;
then G is finite-ind;
hence thesis by A5,A7,Def6;
end;
theorem
G1 is finite-ind & G2 c= G1 implies G2 is finite-ind & ind G2 <= ind G1
proof
assume that
A1: G1 is finite-ind and
A2: G2 c=G1;
A3: -1<=ind G1 by A1,Th11;
then for A st A in G2 holds A is finite-ind & ind A<=ind G1 by A1,A2,Th11;
hence thesis by A3,Th11;
end;
Lm4: for i be Integer st G is finite-ind & G1 is finite-ind & ind G<=i & ind
G1<=i holds G\/G1 is finite-ind & ind(G\/G1)<=i
proof
let i be Integer such that
A1: G is finite-ind and
A2: G1 is finite-ind and
A3: ind G<=i and
A4: ind G1<=i;
A5: for A st A in G\/G1 holds A is finite-ind & ind A<=i
proof
let A;
assume A in G\/G1;
then A in G or A in G1 by XBOOLE_0:def 3;
hence thesis by A1,A2,A3,A4,Th11;
end;
-1<=i by A1,A3,Th11;
hence thesis by A5,Th11;
end;
registration
let T;
let G1,G2 be finite-ind Subset-Family of T;
cluster G1 \/ G2 -> finite-ind for Subset-Family of T;
coherence
proof
set iG1=ind G1+1,iG2=ind G2+1;
-1<=ind G1 by Def6;
then -1+1<=iG1 by XREAL_1:6;
then
A1: iG1 in NAT by INT_1:3;
-1<=ind G2 by Def6;
then -1+1<=iG2 by XREAL_1:6;
then
A2: iG2 in NAT by INT_1:3;
then ind G1+0<=iG1 & iG1<=iG1+iG2 by A1,NAT_1:11,XREAL_1:6;
then
A3: ind G1<=iG1+iG2 by XXREAL_0:2;
ind G2+0<=iG2 & iG2<=iG2+iG1 by A2,A1,NAT_1:11,XREAL_1:6;
then ind G2<=iG1+iG2 by XXREAL_0:2;
hence thesis by A3,Lm4;
end;
end;
theorem
G is finite-ind & G1 is finite-ind & ind G <= I & ind G1 <= I implies
ind (G\/G1) <= I by Lm4;
definition
let T;
func ind T -> Integer equals
ind [#]T;
correctness;
end;
registration
let T be non empty finite-ind TopSpace;
cluster ind T -> natural;
coherence
proof
[#]T is non empty finite-ind by Def4;
hence thesis;
end;
end;
theorem
for X be non empty set holds ind 1TopSp X = 0
proof
let X be non empty set;
set T=1TopSp X;
(Seq_of_ind T).0={{}T} by Def1;
then
A1: not[#]T in (Seq_of_ind T).0 by TARSKI:def 1;
A2: [#]T in (Seq_of_ind T).(0+1) by Lm2;
then [#]T is finite-ind;
hence thesis by A1,A2,Def5;
end;
theorem Th15:
(ex n st for p be Point of T,U be open Subset of T st p in U ex
W be open Subset of T st p in W & W c= U & Fr W is finite-ind & ind Fr W <= n-1
) implies T is finite-ind
proof
given n such that
A1: for p be Point of T,U be open Subset of T st p in U ex W be open
Subset of T st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1;
set CT=[#]T;
set TT=T|CT;
A2: [#]TT=CT by PRE_TOPC:def 5;
T is SubSpace of T by TSEP_1:2;
then
A3: the TopStruct of T=the TopStruct of TT by A2,TSEP_1:5;
now
let p9 be Point of TT,U9 be open Subset of TT such that
A4: p9 in U9;
reconsider p=p9 as Point of T by A2;
U9 in the topology of TT by PRE_TOPC:def 2;
then reconsider U=U9 as open Subset of T by A3,PRE_TOPC:def 2;
consider W be open Subset of T such that
A5: p in W and
A6: W c=U & Fr W is finite-ind & ind Fr W<=n-1 by A1,A4;
W in the topology of T by PRE_TOPC:def 2;
then reconsider W9=W as open Subset of TT by A3,PRE_TOPC:def 2;
take W9;
T is non empty by A5;
then Cl W=Cl W9 & Int W=Int W9 by A2,TOPS_3:54;
then Fr W=Cl W9\Int W9 by TOPGEN_1:8
.=Fr W9 by TOPGEN_1:8;
hence p9 in W9 & W9 c=U9 & Fr W9 in (Seq_of_ind T).n by A5,A6,Th7;
end;
then CT in (Seq_of_ind T).(n+1) by Def1;
then CT is finite-ind;
hence thesis;
end;
theorem Th16:
ind Tf <= n iff for p be Point of Tf,U be open Subset of Tf st p
in U ex W be open Subset of Tf st p in W & W c= U & Fr W is finite-ind & ind Fr
W <= n-1
proof
set CT=[#]Tf;
set TT=Tf|CT;
A1: [#]TT=CT by PRE_TOPC:def 5;
Tf is SubSpace of Tf by TSEP_1:2;
then
A2: the TopStruct of Tf=the TopStruct of TT by A1,TSEP_1:5;
A3: CT is finite-ind by Def4;
hereby
assume
A4: ind Tf<=n;
let p be Point of Tf,U be open Subset of Tf such that
A5: p in U;
reconsider p9=p as Point of TT by A1;
U in the topology of Tf by PRE_TOPC:def 2;
then reconsider U9=U as open Subset of TT by A2,PRE_TOPC:def 2;
consider W9 be open Subset of TT such that
A6: p9 in W9 & W9 c=U9 and
A7: Fr W9 is finite-ind & ind Fr W9<=n-1 by A3,A4,A5,Th9;
W9 in the topology of TT by PRE_TOPC:def 2;
then reconsider W=W9 as open Subset of Tf by A2,PRE_TOPC:def 2;
Tf is non empty by A5;
then Cl W=Cl W9 & Int W=Int W9 by A1,TOPS_3:54;
then
A8: Fr W=Cl W9\Int W9 by TOPGEN_1:8
.=Fr W9 by TOPGEN_1:8;
take W;
Fr W9 in (Seq_of_ind TT).n by A7,Th7;
then
A9: Fr W in (Seq_of_ind Tf).n by A8,Th3;
then Fr W is finite-ind;
hence p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1 by A6,A9,Th7;
end;
assume
A10: for p be Point of Tf,U be open Subset of Tf st p in U ex W be open
Subset of Tf st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1;
now
let p9 be Point of TT,U9 be open Subset of TT such that
A11: p9 in U9;
reconsider p=p9 as Point of Tf by A1;
U9 in the topology of TT by PRE_TOPC:def 2;
then reconsider U=U9 as open Subset of Tf by A2,PRE_TOPC:def 2;
consider W be open Subset of Tf such that
A12: p in W & W c=U and
A13: Fr W is finite-ind & ind Fr W<=n-1 by A10,A11;
W in the topology of Tf by PRE_TOPC:def 2;
then reconsider W9=W as open Subset of TT by A2,PRE_TOPC:def 2;
Tf is non empty by A11;
then Cl W=Cl W9 & Int W=Int W9 by A1,TOPS_3:54;
then
A14: Fr W=Cl W9\Int W9 by TOPGEN_1:8
.=Fr W9 by TOPGEN_1:8;
take W9;
Fr W in (Seq_of_ind Tf).n by A13,Th7;
then
A15: Fr W9 in (Seq_of_ind TT).n by A14,Th3;
then Fr W9 is finite-ind;
hence
p9 in W9 & W9 c=U9 & Fr W9 is finite-ind & ind Fr W9<=n-1 by A12,A15,Th7;
end;
hence thesis by A3,Th9;
end;
Lm5: T|Af is finite-ind & ind T|Af = ind Af
proof
set TA=T|Af;
A1: [#]TA=Af by PRE_TOPC:def 5;
per cases by Th6;
suppose
A2: ind Af=-1;
then Af={}T by Th6;
hence thesis by A2,Th6;
end;
suppose
A3: Af is non empty;
then T is non empty;
then reconsider n=ind Af as Nat by A3,TARSKI:1;
Af in (Seq_of_ind T).(n+1) by Def5;
then
A4: [#]TA in (Seq_of_ind TA).(n+1) by A1,Th3;
then
A5: [#]TA is finite-ind;
hence TA is finite-ind;
A6: ind[#]TA>=n
proof
assume ind[#]TA0;
then reconsider n=n9-1 as Nat by NAT_1:20;
let T such that
A6: T is finite-ind and
A7: ind T=n9-1;
let A be Subset of T;
set TA=T|A;
A8: [#]TA=A by PRE_TOPC:def 5;
A9: now
let p be Point of TA,U be open Subset of TA such that
A10: p in U;
U in the topology of TA by PRE_TOPC:def 2;
then consider U9 be Subset of T such that
A11: U9 in the topology of T and
A12: U=U9/\[#]TA by PRE_TOPC:def 4;
A13: p in U9 by A10,A12,XBOOLE_0:def 4;
then reconsider p9=p as Point of T;
U9 is open Subset of T by A11,PRE_TOPC:def 2;
then consider W9 be open Subset of T such that
A14: p9 in W9 & W9 c=U9 and
A15: Fr W9 is finite-ind and
A16: ind Fr W9<=n-1 by A6,A7,A13,Th16;
reconsider i=ind Fr W9+1 as Nat by A15,Lm3;
ind Fr W9+1-1<=n-1 by A16;
then n9-1 finite-ind for Subset of Tf;
coherence by Lm7;
end;
registration
let T,Af;
cluster T|Af -> finite-ind;
coherence by Lm5;
end;
:: Teoria wymiaru Th 1.1.2
theorem
ind T|Af = ind Af by Lm5;
theorem Th18:
T|A is finite-ind implies A is finite-ind
proof
assume T|A is finite-ind;
then consider n such that
A1: [#](T|A) in (Seq_of_ind(T|A)).n by Def2;
[#](T|A)=A by PRE_TOPC:def 5;
then A in (Seq_of_ind T).n by A1,Th3;
hence thesis;
end;
theorem Th19:
A c= Af implies A is finite-ind & ind A <= ind Af
proof
assume
A1: A c=Af;
[#](T|Af)=Af by PRE_TOPC:def 5;
then reconsider A9=A as Subset of T|Af by A1;
A2: ind T|Af=ind Af by Lm5;
A3: T|Af|A9=T|A by METRIZTS:9;
hence A is finite-ind by Th18;
then ind T|A=ind A by Lm5;
hence thesis by A2,A3,Lm6;
end;
theorem
for A be Subset of Tf holds ind A <= ind Tf by Th19;
theorem Th21:
F = B & B is finite-ind implies F is finite-ind & ind F = ind B
proof
assume that
A1: F=B and
A2: B is finite-ind;
A3: T|A|F=T|B by A1,METRIZTS:9;
then F is finite-ind by A2,Th18;
then ind F=ind(T|A|F) by Lm5
.=ind(T|B) by A1,METRIZTS:9
.=ind B by A2,Lm5;
hence thesis by A2,A3,Th18;
end;
theorem Th22:
F = B & F is finite-ind implies B is finite-ind & ind F = ind B
proof
assume that
A1: F=B and
A2: F is finite-ind;
A3: T|A|F=T|B by A1,METRIZTS:9;
then
A4: B is finite-ind by A2,Th18;
ind F=ind(T|A|F) by A2,Lm5
.=ind(T|B) by A1,METRIZTS:9
.=ind B by A4,Lm5;
hence thesis by A2,A3,Th18;
end;
Lm8: for T1,T2 be TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds
T2 is finite-ind & ind T2<=ind T1
proof
defpred P[Nat] means for T1,T2 be TopSpace st T1,T2 are_homeomorphic & T1 is
finite-ind & ind T1<=$1 holds T2 is finite-ind & ind T2<=ind T1;
let T1,T2 be TopSpace such that
A1: T1,T2 are_homeomorphic and
A2: T1 is finite-ind;
reconsider i=ind T1+1 as Nat by A2,Lm3;
A3: for n st P[n] holds P[n+1]
proof
let n such that
A4: P[n];
set n1=n+1;
let T1,T2 be TopSpace such that
A5: T1,T2 are_homeomorphic and
A6: T1 is finite-ind and
A7: ind T1<=n+1;
consider f be Function of T1,T2 such that
A8: f is being_homeomorphism by A5,T_0TOPSP:def 1;
set f9=f";
A9: dom f=[#]T1 by A8;
A10: rng f=[#]T2 by A8;
A11: f is onto by A10;
A12: f is one-to-one by A8;
per cases;
suppose
A13: [#]T1={}T1;
then ind T1=-1 by Th6;
hence thesis by A10,A13,Th6;
end;
suppose
A14: [#]T1<>{}T1;
then T1 is non empty;
then reconsider i=ind T1 as Nat by A6,TARSKI:1;
A15: T1 is non empty by A14;
A16: T2 is non empty by A9,A14;
per cases by A7,NAT_1:8;
suppose
i<=n;
hence thesis by A4,A5,A6;
end;
suppose
A17: ind T1=n+1;
A18: dom f9=[#]T2 by A10,A12,A16,TOPS_2:49;
A19: for p be Point of T2,U be open Subset of T2 st p in U ex W be
open Subset of T2 st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n1-1
proof
reconsider F=f as Function;
let p be Point of T2,U be open Subset of T2;
assume p in U;
then
A20: f9.p in f9.:U by A18,FUNCT_1:def 6;
f"U=f9.:U & f"U is open by A8,A15,A16,TOPGRP_1:26,TOPS_2:55;
then consider W be open Subset of T1 such that
A21: f9.p in W and
A22: W c=f"U and
A23: Fr W is finite-ind and
A24: ind Fr W<=n1-1 by A6,A17,A20,Th16;
set FW=Fr W;
A25: ind(T1|FW)=ind FW by A23,Lm5;
FW,f.:FW are_homeomorphic by A8,METRIZTS:3;
then
A26: T1|FW,T2|(f.:FW)are_homeomorphic by METRIZTS:def 1;
then T2|(f.:FW) is finite-ind by A4,A23,A24,A25;
then
A27: f.:FW is finite-ind by Th18;
F"=f9 by A11,A12,TOPS_2:def 4;
then
A28: f.(f9.p)=p by A10,A12,A16,FUNCT_1:35;
ind(T2|(f.:FW))<=ind(T1|FW) by A4,A23,A24,A25,A26;
then
A29: ind(T2|(f.:FW))<=n1-1 by A24,A25,XXREAL_0:2;
reconsider W9=f.:W as open Subset of T2 by A8,A15,A16,TOPGRP_1:25;
take W9;
W9 c=f.:(f"U) by A22,RELAT_1:123;
hence p in W9 & W9 c=U by A9,A10,A21,A28,FUNCT_1:77,def 6;
f.:FW=f.:(Cl W\W) by TOPS_1:42
.=f.:(Cl W)\W9 by A12,FUNCT_1:64
.=Cl W9\W9 by A8,A16,TOPS_2:60
.=Fr W9 by TOPS_1:42;
hence thesis by A27,A29,Lm5;
end;
then T2 is finite-ind by Th15;
hence thesis by A17,A19,Th16;
end;
end;
end;
A30: P[0]
proof
let T1,T2 be TopSpace such that
A31: T1,T2 are_homeomorphic and
A32: T1 is finite-ind and
A33: ind T1<=0;
consider f be Function of T1,T2 such that
A34: f is being_homeomorphism by A31,T_0TOPSP:def 1;
set f9=f";
A35: dom f=[#]T1 by A34;
A36: rng f=[#]T2 by A34;
A37: f is onto by A36;
A38: f is one-to-one by A34;
per cases;
suppose
A39: [#]T1={}T1;
then ind T1=-1 by Th6;
hence thesis by A36,A39,Th6;
end;
suppose
A40: [#]T1<>{}T1;
then T1 is non empty;
then reconsider i=ind T1 as Nat by A32,TARSKI:1;
A41: i=0 by A33;
A42: T1 is non empty by A40;
A43: T2 is non empty by A35,A40;
then
A44: dom f9=[#]T2 by A36,A38,TOPS_2:49;
A45: for p be Point of T2,U be open Subset of T2 st p in U ex W be open
Subset of T2 st p in W & W c=U & Fr W is finite-ind & ind Fr W<=0-1
proof
reconsider F=f as Function;
let p be Point of T2,U be open Subset of T2;
assume p in U;
then
A46: f9.p in f9.:U by A44,FUNCT_1:def 6;
F"=f9 by A37,A38,TOPS_2:def 4;
then
A47: f.(f9.p)=p by A36,A38,A43,FUNCT_1:35;
f"U=f9.:U & f"U is open by A34,A42,A43,TOPGRP_1:26,TOPS_2:55;
then consider W be open Subset of T1 such that
A48: f9.p in W and
A49: W c=f"U and
A50: Fr W is finite-ind and
A51: ind Fr W<=0-1 by A32,A33,A46,Th16;
reconsider W9=f.:W as open Subset of T2 by A34,A42,A43,TOPGRP_1:25;
take W9;
W9 c=f.:(f"U) by A49,RELAT_1:123;
hence p in W9 & W9 c=U by A35,A36,A47,A48,FUNCT_1:77,def 6;
ind Fr W>=-1 by A50,Th5;
then ind Fr W=-1 by A51,XXREAL_0:1;
then Fr W={}T1 by A50,Th6;
then W is closed by TOPGEN_1:14;
then W9 is closed by A34,A43,TOPS_2:58;
then Fr W9={}T2 by TOPGEN_1:14;
hence thesis by Th6;
end;
then T2 is finite-ind by Th15;
hence thesis by A41,A45,Th16;
end;
end;
A52: for n holds P[n] from NAT_1:sch 2(A30,A3);
ind T1+0<=i by XREAL_1:6;
hence thesis by A1,A2,A52;
end;
Lm9: for T1,T2 be TopSpace st T1,T2 are_homeomorphic holds(T1 is finite-ind
iff T2 is finite-ind) & (T1 is finite-ind implies ind T2=ind T1)
proof
let T1,T2 be TopSpace such that
A1: T1,T2 are_homeomorphic;
consider f be Function of T1,T2 such that
A2: f is being_homeomorphism by A1,T_0TOPSP:def 1;
A3: dom f=[#]T1 by A2;
A4: rng f=[#]T2 by A2;
per cases;
suppose
A5: [#]T1={}T1;
then ind[#]T2=-1 by A4,Th6;
hence thesis by A4,A5,Th6;
end;
suppose
T1 is non empty;
then reconsider t1=T1,t2=T2 as non empty TopSpace by A3;
A6: t2,t1 are_homeomorphic by A1;
hence T1 is finite-ind iff T2 is finite-ind by Lm8;
assume
A7: T1 is finite-ind;
then T2 is finite-ind by A1,Lm8;
then
A8: ind T1<=ind T2 by A6,Lm8;
ind T2<=ind T1 by A1,A7,Lm8;
hence thesis by A8,XXREAL_0:1;
end;
end;
:: Teoria wymiaru Th 1.1.4
theorem
for T be non empty TopSpace st T is regular holds T is finite-ind &
ind T <= n iff for A be closed Subset of T,p be Point of T st not p in A ex L
be Subset of T st L separates{p},A & L is finite-ind & ind L <= n-1
proof
let T be non empty TopSpace such that
A1: T is regular;
hereby
assume
A2: T is finite-ind & ind T<=n;
let A be closed Subset of T,p be Point of T;
assume not p in A;
then p in A` by XBOOLE_0:def 5;
then consider V1,V2 be Subset of T such that
A3: V1 is open and
A4: V2 is open and
A5: p in V1 and
A6: A c=V2 and
A7: V1 misses V2 by A1,PRE_TOPC:def 11;
A8: V2`c=A` by A6,SUBSET_1:12;
consider W1 be open Subset of T such that
A9: p in W1 and
A10: W1 c=V1 and
A11: Fr W1 is finite-ind & ind Fr W1<=n-1 by A2,A3,A5,Th16;
take L=Fr W1;
A12: L =(Cl W1\W1)`` by TOPS_1:42
.=(([#]T\Cl W1)\/[#]T/\W1)` by XBOOLE_1:52
.=((Cl W1)`\/W1)` by XBOOLE_1:28;
V2 misses Cl V1 by A4,A7,TSEP_1:36;
then
A13: Cl V1 c=V2` by SUBSET_1:23;
Cl W1 c=Cl V1 by A10,PRE_TOPC:19;
then Cl W1 c=V2` by A13;
then Cl W1 c=A` by A8;
then
A14: A c=(Cl W1)` by SUBSET_1:16;
W1 c=Cl W1 by PRE_TOPC:18;
then
A15: (Cl W1)`misses W1 by SUBSET_1:24;
{p}c=W1 by A9,ZFMISC_1:31;
hence L separates{p},A & L is finite-ind & ind L<=n-1 by A11,A12,A14,A15,
METRIZTS:def 3;
end;
assume
A16: for A be closed Subset of T,p be Point of T st not p in A ex L be
Subset of T st L separates{p},A & L is finite-ind & ind L<=n-1;
A17: for p be Point of T,U be open Subset of T st p in U ex W be open Subset
of T st p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1
proof
let p be Point of T,U be open Subset of T;
assume p in U;
then not p in U` by XBOOLE_0:def 5;
then consider L be Subset of T such that
A18: L separates{p},U` and
A19: L is finite-ind and
A20: ind L<=n-1 by A16;
consider A1,A2 be open Subset of T such that
A21: {p}c=A1 and
A22: U`c=A2 and
A23: A1 misses A2 and
A24: L=(A1\/A2)` by A18,METRIZTS:def 3;
A25: A2`c=U & A1 c=A2` by A22,A23,SUBSET_1:17,23;
take A1;
Cl A1 misses A2 by A23,TSEP_1:36;
then Cl A1\A2=Cl A1 by XBOOLE_1:83;
then Fr A1=Cl A1\A2\A1 by TOPS_1:42
.=Cl A1\(A2\/A1) by XBOOLE_1:41;
then
A26: Fr A1 c=L by A24,XBOOLE_1:33;
then ind Fr A1<=ind L by A19,Th19;
hence thesis by A19,A20,A21,A25,A26,Th19,XXREAL_0:2,ZFMISC_1:31;
end;
then T is finite-ind by Th15;
hence thesis by A17,Th16;
end;
theorem
T1,T2 are_homeomorphic implies (T1 is finite-ind iff T2 is finite-ind)
by Lm9;
theorem
T1,T2 are_homeomorphic & T1 is finite-ind implies ind T1 = ind T2 by Lm9;
theorem Th26:
for A1 be Subset of T1,A2 be Subset of T2 st A1,A2
are_homeomorphic holds A1 is finite-ind iff A2 is finite-ind
proof
let A1 be Subset of T1,A2 be Subset of T2;
assume A1,A2 are_homeomorphic;
then
A1: T1|A1,T2|A2 are_homeomorphic by METRIZTS:def 1;
hereby
assume A1 is finite-ind;
then T2|A2 is finite-ind by A1,Lm9;
hence A2 is finite-ind by Th18;
end;
assume A2 is finite-ind;
then T1|A1 is finite-ind by A1,Lm9;
hence thesis by Th18;
end;
theorem
for A1 be Subset of T1,A2 be Subset of T2 st A1,A2 are_homeomorphic &
A1 is finite-ind holds ind A1 = ind A2
proof
let A1 be Subset of T1,A2 be Subset of T2 such that
A1: A1,A2 are_homeomorphic and
A2: A1 is finite-ind;
T1|A1,T2|A2 are_homeomorphic by A1,METRIZTS:def 1;
then
A3: ind T1|A1=ind T2|A2 by A2,Lm9;
A2 is finite-ind & ind T1|A1=ind A1 by A1,A2,Lm5,Th26;
hence thesis by A3,Lm5;
end;
theorem
[:T1,T2:] is finite-ind implies [:T2,T1:] is finite-ind & ind [:T1,T2
:] = ind [:T2,T1:]
proof
assume
A1: [:T1,T2:] is finite-ind;
per cases;
suppose
A2: T1 is empty or T2 is empty;
then ind[:T1,T2:]=-1 by Th6;
hence thesis by A2,Th6;
end;
suppose
T1 is non empty & T2 is non empty;
then [:T1,T2:],[:T2,T1:]are_homeomorphic by YELLOW12:44;
hence thesis by A1,Lm9;
end;
end;
theorem
for Ga be Subset-Family of T|A st Ga is finite-ind & Ga = G holds G is
finite-ind & ind G = ind Ga
proof
let G1 be Subset-Family of T|A such that
A1: G1 is finite-ind and
A2: G1=G;
A3: for B be Subset of T st B in G holds B is finite-ind & ind B<= ind G1
proof
let B be Subset of T;
assume
A4: B in G;
then reconsider B9=B as Subset of T|A by A2;
A5: B9 is finite-ind by A1,A2,A4;
then ind B=ind B9 by Th22;
hence thesis by A1,A2,A4,A5,Th11,Th22;
end;
A6: -1<=ind G1 by A1,Th11;
then
A7: ind G<=ind G1 by A3,Th11;
A8: G is finite-ind by A3,A6,Th11;
A9: for B be Subset of T|A st B in G1 holds B is finite-ind & ind B <=ind G
proof
let B be Subset of T|A;
assume
A10: B in G1;
then reconsider B9=B as Subset of T by A2;
B9 is finite-ind by A2,A3,A10;
then ind B=ind B9 by Th21;
hence thesis by A1,A2,A8,A10,Th11;
end;
-1<=ind G by A8,Th11;
then ind G1<=ind G by A9,Th11;
hence thesis by A3,A6,A7,Th11,XXREAL_0:1;
end;
theorem
for Ga be Subset-Family of T|A st G is finite-ind & Ga = G holds Ga is
finite-ind & ind G = ind Ga
proof
let G1 be Subset-Family of T|A such that
A1: G is finite-ind and
A2: G1=G;
A3: for B be Subset of T|A st B in G1 holds B is finite-ind & ind B <=ind G
proof
let B be Subset of T|A;
assume
A4: B in G1;
then reconsider B9=B as Subset of T by A2;
A5: B9 is finite-ind by A1,A2,A4;
then ind B=ind B9 by Th21;
hence thesis by A1,A2,A4,A5,Th11,Th21;
end;
A6: -1<=ind G by A1,Th11;
then
A7: ind G1<=ind G by A3,Th11;
A8: G1 is finite-ind by A3,A6,Th11;
A9: for B be Subset of T st B in G holds B is finite-ind & ind B<= ind G1
proof
let B be Subset of T;
assume
A10: B in G;
then reconsider B9=B as Subset of T|A by A2;
B9 is finite-ind by A2,A3,A10;
then ind B=ind B9 by Th22;
hence thesis by A1,A2,A8,A10,Th11;
end;
-1<=ind G1 by A8,Th11;
then ind G<=ind G1 by A9,Th11;
hence thesis by A3,A6,A7,Th11,XXREAL_0:1;
end;
begin :: Basic Properties for zero dimensional Topological Spaces
:: Teoria wymiaru Th 1.1.6
theorem Th31:
T is finite-ind & ind T <= n iff ex Bas be Basis of T st for A
st A in Bas holds Fr A is finite-ind & ind Fr A <= n-1
proof
set TOP=the topology of T;
set cT=the carrier of T;
hereby
defpred P[object,object] means
for p be Point of T,A be Subset of T st$1=[p,A]
holds$2 in TOP & (not p in A implies $2={}T) & (p in A implies ex W be open
Subset of T st W=$2 & p in W & W c=A & ind Fr W<=n-1);
assume that
A1: T is finite-ind and
A2: ind T<=n;
A3: for x be object st x in [:cT,TOP:]ex y be object st P[x,y]
proof
let x be object;
assume x in [:cT,TOP:];
then consider p9,A9 be object such that
A4: p9 in cT and
A5: A9 in TOP and
A6: x=[p9,A9] by ZFMISC_1:def 2;
reconsider p9 as Point of T by A4;
reconsider A9 as open Subset of T by A5,PRE_TOPC:def 2;
per cases;
suppose
A7: not p9 in A9;
take{}T;
let p be Point of T,A such that
A8: x=[p,A];
p=p9 by A6,A8,XTUPLE_0:1;
hence thesis by A6,A7,A8,PRE_TOPC:def 2,XTUPLE_0:1;
end;
suppose
p9 in A9;
then consider W be open Subset of T such that
A9: p9 in W & W c=A9 and
Fr W is finite-ind and
A10: ind Fr W<=n-1 by A1,A2,Th16;
take W;
let p be Point of T,A;
assume x=[p,A];
then p=p9 & A=A9 by A6,XTUPLE_0:1;
hence thesis by A9,A10,PRE_TOPC:def 2;
end;
end;
consider f be Function such that
A11: dom f=[:cT,TOP:] and
A12: for x be object st x in [:cT,TOP:] holds P[x,f.x]
from CLASSES1:sch
1(A3);
A13: rng f c=TOP
proof
let y be object;
assume y in rng f;
then consider x be object such that
A14: x in dom f and
A15: f.x=y by FUNCT_1:def 3;
ex p,A be object st p in cT & A in TOP & x=[p,A]
by A11,A14,ZFMISC_1:def 2;
hence thesis by A11,A12,A14,A15;
end;
then reconsider RNG=rng f as Subset-Family of T by XBOOLE_1:1;
now
let A be Subset of T;
assume A is open;
then
A16: A in TOP by PRE_TOPC:def 2;
let p be Point of T such that
A17: p in A;
A18: [p,A] in [:cT,TOP:] by A16,A17,ZFMISC_1:87;
then consider W be open Subset of T such that
A19: W=f.[p,A] & p in W & W c=A and
ind Fr W<=n-1 by A12,A17;
reconsider W as Subset of T;
take W;
thus W in RNG & p in W & W c=A by A11,A18,A19,FUNCT_1:def 3;
end;
then reconsider RNG as Basis of T by A13,YELLOW_9:32;
take RNG;
let B be Subset of T;
assume B in RNG;
then consider x be object such that
A20: x in dom f and
A21: f.x=B by FUNCT_1:def 3;
consider p,A be object such that
A22: p in cT and
A23: A in TOP and
A24: x=[p,A] by A11,A20,ZFMISC_1:def 2;
reconsider A as set by TARSKI:1;
per cases;
suppose
p in A;
then
ex W be open Subset of T st W=f.[p,A] & p in W & W c=A & ind Fr W<=
n-1 by A11,A12,A20,A23,A24;
hence Fr B is finite-ind & ind Fr B<=n-1 by A1,A21,A24;
end;
suppose
A25: not p in A;
A26: T is non empty by A22;
B={}T by A11,A12,A20,A21,A22,A23,A24,A25;
then
A27: Fr B={}T by A26,TOPGEN_1:39;
0-1<=n-1 by XREAL_1:9;
hence Fr B is finite-ind & ind Fr B<=n-1 by A27,Th6;
end;
end;
given B be Basis of T such that
A28: for A be Subset of T st A in B holds Fr A is finite-ind & ind Fr A <=n-1;
A29: now
let p be Point of T,U be open Subset of T;
assume p in U;
then consider W be Subset of T such that
A30: W in B and
A31: p in W & W c=U by YELLOW_9:31;
B c=TOP by TOPS_2:64;
then reconsider W as open Subset of T by A30,PRE_TOPC:def 2;
take W;
thus p in W & W c=U & Fr W is finite-ind & ind Fr W<=n-1 by A28,A30,A31;
end;
then T is finite-ind by Th15;
hence thesis by A29,Th16;
end;
:: Wprowadzenie do topologi 3.4.2 "=>"
theorem Th32:
for T st T is T_1 & for A,B be closed Subset of T st A misses B
ex A9,B9 be closed Subset of T st A9 misses B9 & A9\/B9 = [#]T & A c= A9 & B c=
B9 holds T is finite-ind & ind T <= 0
proof
let T such that
A1: T is T_1 & for A,B be closed Subset of T st A misses B ex A9,B9 be
closed Subset of T st A9 misses B9 & A9\/B9=[#]T & A c=A9 & B c=B9;
A2: now
let p be Point of T,U be open Subset of T such that
A3: p in U;
reconsider P={p} as Subset of T by A3,ZFMISC_1:31;
not p in U` by A3,XBOOLE_0:def 5;
then
A4: P misses U` by ZFMISC_1:50;
T is non empty by A3;
then consider A9,B9 be closed Subset of T such that
A5: A9 misses B9 and
A6: A9\/B9=[#]T and
A7: P c=A9 and
A8: U`c=B9 by A1,A4;
reconsider W=B9` as open Subset of T;
take W;
p in P by TARSKI:def 1;
then U``=U & not p in B9 by A5,A7,XBOOLE_0:3;
hence p in W & W c=U by A3,A8,SUBSET_1:12,XBOOLE_0:def 5;
B9=A9` by A5,A6,PRE_TOPC:5;
then Fr B9={}T by TOPGEN_1:14;
hence Fr W is finite-ind & ind Fr W<=0-1 by Th6;
end;
then T is finite-ind by Th15;
hence thesis by A2,Th16;
end;
theorem Th33:
for X be set,f be SetSequence of X ex g be SetSequence of X st
union rng f = union rng g & (for i,j be Nat st i<>j holds g.i misses g.j) & for
n ex fn be finite Subset-Family of X st fn={f.i where i is Element of NAT:ij holds g.i misses g.j
proof
let i,j be Nat;
assume i<>j;
then i*