:: Small {I}nductive {D}imension of {T}opological {S}paces
:: by Karol P\c{a}k
::
:: Received June 29, 2009
:: Copyright (c) 2009 Association of Mizar Users
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;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
ORDINAL1, MCART_1, FUNCT_2, CARD_1, CARD_3, CANTOR_1, FINSET_1, NUMBERS,
ZFMISC_1, XXREAL_0, REAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC, TOPS_1, TOPS_2,
NAT_1, STRUCT_0, COMPTS_1, PCOMPS_1, PROB_1, WAYBEL23, BORSUK_1,
BORSUK_3, INT_1, METRIZTS;
constructors SETFAM_1, TOPS_1, TOPS_2, BORSUK_1, REAL_1, KURATO_2, CANTOR_1,
WELLFND1, WAYBEL23, COMPTS_1, BORSUK_3, TSP_1, METRIZTS, RELSET_1,
ORDINAL2;
registrations BORSUK_3, CARD_1, COMPTS_1, FINSET_1, FUNCT_2, INT_1, NAT_1,
ORDINAL1, PRE_TOPC, RELAT_1, STRUCT_0, SUBSET_1, TOPREAL6, TOPS_1,
XBOOLE_0, XCMPLX_0, XREAL_0, XXREAL_0, YELLOW13, METRIZTS, RELSET_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions COMPTS_1, STRUCT_0, SUBSET_1, TOPS_1, TOPS_2, TARSKI, XBOOLE_0;
theorems CANTOR_1, CARD_2, CARD_3, FUNCT_1, FUNCT_2, INT_1, KURATO_2,
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;
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 10;
[#](T|A)c=[#]T by PRE_TOPC:def 9;
then reconsider F'=F,Fd=F` as Subset of T by XBOOLE_1:1;
assume
A2: F=B/\A;
then Cl F' c=Cl B by PRE_TOPC:49,XBOOLE_1:18;
then Cl F'/\A c=Cl B/\A by XBOOLE_1:26;
then
A3: Cl F c=Cl B/\A by A1,PRE_TOPC:47;
[#](T|A)=A by PRE_TOPC:def 10;
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:49;
then
A4: Cl Fd/\A c=Cl B`/\A by XBOOLE_1:26;
Cl F`=Cl Fd/\[#](T|A) by PRE_TOPC:47;
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 18;
A1 misses B1` by A4,SUBSET_1:44;
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 18;
A12: Cl C2`=C2` & C2`c=B1 by A8,A10,PRE_TOPC:52,SUBSET_1:36;
A2 misses B2` by A5,SUBSET_1:44;
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 18;
reconsider C1,D1 as open Subset of T by A13,A7;
take C1,D1;
D1 c=D2` by A17,SUBSET_1:43;
then
A18: Cl D1 c=Cl D2` by PRE_TOPC:49;
C1 c=C2` by A11,SUBSET_1:43;
then Cl C1 c=Cl C2` by PRE_TOPC:49;
then
A19: Cl C1 c=B1 by A12,XBOOLE_1:1;
Cl D2`=D2` & D2`c=B2 by A14,A16,PRE_TOPC:52,SUBSET_1:36;
then Cl D1 c=B2 by A18,XBOOLE_1:1;
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:48;
hence thesis by A21,XBOOLE_1:64;
end;
hence thesis by PRE_TOPC:def 18;
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 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[set,set] means A in $2 iff A in $1 or for p,U st p in U ex W st
p in W & W c=U & Fr W in $1;
set C = the carrier of T;
reconsider E={{}T} as Element of bool bool C;
A1: for x be set st x in bool bool C ex y be set st y in bool bool C & P[x
,y]
proof
let x be set such that
x in bool bool C;
defpred Q[set] means for A st A=$1 holds A in x or for p,U st p in U ex
W st p in W & W c=U & Fr W in x;
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;
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 set 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 Function of NAT,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;
take f;
now
let n;
f.(n+1)=p/.(f.n) by A5
.=p.(f.n);
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 A3;
end;
hence thesis by A4;
end;
uniqueness
proof
let Ind1,Ind2 be SetSequence of bool the carrier of T such that
A6: 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
A7: 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;
A8: for n be Element of NAT st P[n] holds P[n+1]
proof
let n be Element of NAT such that
A9: P[n];
thus Ind1.(n+1)c=Ind2.(n+1)
proof
let x be set such that
A10: x in Ind1.(n+1);
reconsider A=x as Subset of T by A10;
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 A6,A10;
hence thesis by A7,A9;
end;
let x be set such that
A11: x in Ind2.(n+1);
reconsider A=x as Subset of T by A11;
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 A7,A11;
hence thesis by A6,A9;
end;
A12: P[0] by A6,A7;
for n be Element of NAT holds P[n] from NAT_1:sch 1(A12,A8);
hence thesis by FUNCT_2:113;
end;
end;
registration
let T;
cluster Seq_of_ind T -> non-descending;
coherence
proof
now
let n be Element of NAT;
thus (Seq_of_ind T).n c=(Seq_of_ind T).(n+1)
proof
let x be set;
assume
x in (Seq_of_ind T).n;
hence thesis by Def1;
end;
end;
hence thesis by KURATO_2:def 6;
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 9;
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 U'=U as open Subset of TAF by A4;
consider W' be open Subset of TAF such that
A9: p in W' & W' c=U' & Fr W' in (Seq_of_ind TA).n by A7,A8;
reconsider W=W' 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;
reconsider p'=p as Point of TAF by A3,METRIZTS:9;
end;
hence B in (Seq_of_ind T).n1 by Def1;
end;
end;
A10: [#]TAF c=[#]TA by PRE_TOPC:def 9;
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 U'=U as open Subset of TB by A4;
consider W' be open Subset of TB such that
A14: p in W' & W' c=U' & Fr W' in (Seq_of_ind T).n by A12,A13;
reconsider W=W' 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;
reconsider p'=p as Point of TB by A3,METRIZTS:9;
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
:Def3:
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 Th4:
A in G & G is finite-ind implies A is finite-ind
proof
assume that
A1: A in G and
A2: G is finite-ind;
ex n st G c=(Seq_of_ind T).n by A2,Def3;
hence thesis by A1,Def2;
end;
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:37;
then
A6: Fr W=Cl W\W & A\W c=A\{p} by TOPS_1:76,XBOOLE_1:34;
thus p in W & W c=U by A5;
[#](T|A)c=[#]T by PRE_TOPC:def 9;
then reconsider FrW=Fr W as Subset of T by XBOOLE_1:1;
A7: A\{p}c=A & not p in A\{p} by XBOOLE_1:36,ZFMISC_1:64;
A8: [#](T|A)=A by PRE_TOPC:def 10;
then p in A by A5;
then
A9: A\{p}c finite-ind Subset of T;
coherence by Lm1;
cluster empty -> finite-ind Subset-Family of T;
coherence
proof
let G;
assume
G is empty;
then
A1: G c={{}T} by XBOOLE_1:2;
(Seq_of_ind T).0={{}T} by Def1;
hence thesis by A1,Def3;
end;
cluster non empty finite-ind Subset-Family of T;
existence
proof
(Seq_of_ind T).0={{}T} by Def1;
then {{}T} is finite-ind by Def3;
hence thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster non empty finite-ind Subset of T;
existence
proof
consider x be set such that
A1: x in [#]T by XBOOLE_0:def 1;
{x} is Subset of T by A1,ZFMISC_1:37;
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 TopSpace;
coherence
proof
let T;
assume
T is empty;
then [#]T is finite-ind;
hence thesis by Def4;
end;
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 10;
then reconsider W'=U as Subset of T;
W'` is open by PRE_TOPC:def 5;
then W' is open & W' is closed by PRE_TOPC:def 5,TOPS_1:29;
then Fr W'={}T by TOPGEN_1:16;
then
A3: Fr W'/\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 by Def2;
hence thesis by Def4;
end;
end;
registration
cluster non empty finite-ind TopSpace;
existence
proof
take T=1TopSp the non empty set;
thus thesis;
end;
end;
reserve Af,Bf 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,Def2;
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 4;
then reconsider i=I as Element of NAT;
MIN<=i by A4,A5;
then MIN*I2;
then
A11: I1>=i21 by INT_1:20;
then reconsider i1=I1 as Element of NAT by INT_1:16;
(Seq_of_ind T).i21 c=(Seq_of_ind T).i1 by A11,PROB_1:def 7;
hence contradiction by A7,A8;
end;
I2<=I1
proof
assume
I1=i11 by INT_1:20;
then reconsider i2=I2 as Element of NAT by INT_1:16;
(Seq_of_ind T).i11 c=(Seq_of_ind T).i2 by A12,PROB_1:def 7;
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 4;
0=-1+1;
hence thesis by A1,XREAL_1:8;
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 4;
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 4;
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:20;
then ind A in NAT by INT_1:16;
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:8;
I+1 in NAT & n in NAT by A2,ORDINAL1:def 13;
then (Seq_of_ind T).(I+1)c=(Seq_of_ind T).n by A3,PROB_1:def 7;
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:20;
then n in NAT & I in NAT by INT_1:16;
then (Seq_of_ind T).n c=(Seq_of_ind T).I by A5,PROB_1:def 7;
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,Def3;
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:8;
then i+1 in NAT by INT_1:16;
then reconsider I1=i+1 as Nat;
MIN=I+1 & MIN<=I1 by A4,A7;
hence I<=i by XREAL_1:8;
end;
I>=0-1 by XREAL_1:11;
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,Def3;
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,Def3,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:8;
then ind G+1 in NAT by INT_1:16;
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,Th4;
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:8;
then reconsider I1=I+1 as Element of NAT by INT_1:16;
A7: G c=(Seq_of_ind T).I1
proof
let x be set 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 by Def3;
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 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:8;
then
A1: iG1 in NAT by INT_1:16;
-1<=ind G2 by Def6;
then -1+1<=iG2 by XREAL_1:8;
then
A2: iG2 in NAT by INT_1:16;
then ind G1+0<=iG1 & iG1<=iG1+iG2 by A1,NAT_1:11,XREAL_1:8;
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:8;
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 by Def2;
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 10;
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 p' be Point of TT,U' be open Subset of TT such that
A4: p' in U';
reconsider p=p' as Point of T by A2;
U' in the topology of TT by PRE_TOPC:def 5;
then reconsider U=U' as open Subset of T by A3,PRE_TOPC:def 5;
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 5;
then reconsider W'=W as open Subset of TT by A3,PRE_TOPC:def 5;
take W';
T is non empty by A5;
then Cl W=Cl W' & Int W=Int W' by A2,TOPS_3:54;
then Fr W=Cl W'\Int W' by TOPGEN_1:10
.=Fr W' by TOPGEN_1:10;
hence p' in W' & W' c=U' & Fr W' 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 by Def2;
hence thesis by Def4;
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 10;
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 p'=p as Point of TT by A1;
U in the topology of Tf by PRE_TOPC:def 5;
then reconsider U'=U as open Subset of TT by A2,PRE_TOPC:def 5;
consider W' be open Subset of TT such that
A6: p' in W' & W' c=U' and
A7: Fr W' is finite-ind & ind Fr W'<=n-1 by A3,A4,A5,Th9;
W' in the topology of TT by PRE_TOPC:def 5;
then reconsider W=W' as open Subset of Tf by A2,PRE_TOPC:def 5;
Tf is non empty by A5;
then Cl W=Cl W' & Int W=Int W' by A1,TOPS_3:54;
then
A8: Fr W=Cl W'\Int W' by TOPGEN_1:10
.=Fr W' by TOPGEN_1:10;
take W;
Fr W' 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 by Def2;
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 p' be Point of TT,U' be open Subset of TT such that
A11: p' in U';
reconsider p=p' as Point of Tf by A1;
U' in the topology of TT by PRE_TOPC:def 5;
then reconsider U=U' as open Subset of Tf by A2,PRE_TOPC:def 5;
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 5;
then reconsider W'=W as open Subset of TT by A2,PRE_TOPC:def 5;
Tf is non empty by A11;
then Cl W=Cl W' & Int W=Int W' by A1,TOPS_3:54;
then
A14: Fr W=Cl W'\Int W' by TOPGEN_1:10
.=Fr W' by TOPGEN_1:10;
take W';
Fr W in (Seq_of_ind Tf).n by A13,Th7;
then
A15: Fr W' in (Seq_of_ind TT).n by A14,Th3;
then Fr W' is finite-ind by Def2;
hence
p' in W' & W' c=U' & Fr W' is finite-ind & ind Fr W'<=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 10;
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;
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 by Def2;
hence TA is finite-ind by Def4;
A6: ind[#]TA>=n
proof
assume
ind[#]TA0;
then reconsider n=n'-1 as Nat by NAT_1:20;
let T such that
A6: T is finite-ind and
A7: ind T=n'-1;
let A be Subset of T;
set TA=T|A;
A8: [#]TA=A by PRE_TOPC:def 10;
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 5;
then consider U' be Subset of T such that
A11: U' in the topology of T and
A12: U=U'/\[#]TA by PRE_TOPC:def 9;
A13: p in U' by A10,A12,XBOOLE_0:def 4;
then reconsider p'=p as Point of T;
U' is open Subset of T by A11,PRE_TOPC:def 5;
then consider W' be open Subset of T such that
A14: p' in W' & W' c=U' and
A15: Fr W' is finite-ind and
A16: ind Fr W'<=n-1 by A6,A7,A13,Th16;
reconsider i=ind Fr W'+1 as Nat by A15,Lm3;
ind Fr W'+1-1<=n-1 by A16;
then n'-1 finite-ind 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 10;
then A in (Seq_of_ind T).n by A1,Th3;
hence thesis by Def2;
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 10;
then reconsider A'=A as Subset of T|Af by A1;
A2: ind T|Af=ind Af by Lm5;
A3: T|Af|A'=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 f'=f";
A9: dom f=[#]T1 by A8,TOPS_2:def 5;
A10: rng f=[#]T2 by A8,TOPS_2:def 5;
A11: f is one-to-one by A8,TOPS_2:def 5;
per cases;
suppose
A12: [#]T1={}T1;
then ind T1=-1 by Th6;
hence thesis by A10,A12,Def4,Th6;
end;
suppose
A13: [#]T1<>{}T1;
then T1 is non empty;
then reconsider i=ind T1 as Nat by A6;
A14: T1 is non empty by A13;
A15: T2 is non empty by A9,A13;
per cases by A7,NAT_1:8;
suppose
i<=n;
hence thesis by A4,A5,A6;
end;
suppose
A16: ind T1=n+1;
A17: dom f'=[#]T2 by A10,A11,A15,TOPS_2:62;
A18: 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
A19: f'.p in f'.:U by A17,FUNCT_1:def 12;
f"U=f'.:U & f"U is open by A8,A10,A11,A14,A15,TOPGRP_1:26,
TOPS_2:68;
then consider W be open Subset of T1 such that
A20: f'.p in W and
A21: W c=f"U and
A22: Fr W is finite-ind and
A23: ind Fr W<=n1-1 by A6,A16,A19,Th16;
set FW=Fr W;
A24: ind(T1|FW)=ind FW by A22,Lm5;
FW,f.:FW are_homeomorphic by A8,METRIZTS:3;
then
A25: T1|FW,T2|(f.:FW)are_homeomorphic by METRIZTS:def 1;
then T2|(f.:FW) is finite-ind by A4,A22,A23,A24;
then
A26: f.:FW is finite-ind by Th18;
F"=f' by A10,A11,TOPS_2:def 4;
then
A27: f.(f'.p)=p by A10,A11,A15,FUNCT_1:57;
ind(T2|(f.:FW))<=ind(T1|FW) by A4,A22,A23,A24,A25;
then
A28: ind(T2|(f.:FW))<=n1-1 by A23,A24,XXREAL_0:2;
reconsider W'=f.:W as open Subset of T2 by A8,A14,A15,TOPGRP_1:25;
take W';
W' c=f.:(f"U) by A21,RELAT_1:156;
hence p in W' & W' c=U by A9,A10,A20,A27,FUNCT_1:147,def 12;
f.:FW=f.:(Cl W\W) by TOPS_1:76
.=f.:(Cl W)\W' by A11,FUNCT_1:123
.=Cl W'\W' by A8,A15,TOPS_2:74
.=Fr W' by TOPS_1:76;
hence thesis by A26,A28,Lm5;
end;
then T2 is finite-ind by Th15;
hence thesis by A16,A18,Th16;
end;
end;
end;
A29: P[0]
proof
let T1,T2 be TopSpace such that
A30: T1,T2 are_homeomorphic and
A31: T1 is finite-ind and
A32: ind T1<=0;
consider f be Function of T1,T2 such that
A33: f is being_homeomorphism by A30,T_0TOPSP:def 1;
set f'=f";
A34: dom f=[#]T1 by A33,TOPS_2:def 5;
A35: rng f=[#]T2 by A33,TOPS_2:def 5;
A36: f is one-to-one by A33,TOPS_2:def 5;
per cases;
suppose
A37: [#]T1={}T1;
then ind T1=-1 by Th6;
hence thesis by A35,A37,Def4,Th6;
end;
suppose
A38: [#]T1<>{}T1;
then T1 is non empty;
then reconsider i=ind T1 as Nat by A31;
A39: i=0 by A32;
A40: T1 is non empty by A38;
A41: T2 is non empty by A34,A38;
then
A42: dom f'=[#]T2 by A35,A36,TOPS_2:62;
A43: 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
A44: f'.p in f'.:U by A42,FUNCT_1:def 12;
F"=f' by A35,A36,TOPS_2:def 4;
then
A45: f.(f'.p)=p by A35,A36,A41,FUNCT_1:57;
f"U=f'.:U & f"U is open by A33,A35,A36,A40,A41,TOPGRP_1:26,TOPS_2
:68;
then consider W be open Subset of T1 such that
A46: f'.p in W and
A47: W c=f"U and
A48: Fr W is finite-ind and
A49: ind Fr W<=0-1 by A31,A32,A44,Th16;
reconsider W'=f.:W as open Subset of T2 by A33,A40,A41,TOPGRP_1:25;
take W';
W' c=f.:(f"U) by A47,RELAT_1:156;
hence p in W' & W' c=U by A34,A35,A45,A46,FUNCT_1:147,def 12;
ind Fr W>=-1 by A48,Th5;
then ind Fr W=-1 by A49,XXREAL_0:1;
then Fr W={}T1 by A48,Th6;
then W is closed by TOPGEN_1:16;
then W' is closed by A33,A41,TOPS_2:72;
then Fr W'={}T2 by TOPGEN_1:16;
hence thesis by Th6;
end;
then T2 is finite-ind by Th15;
hence thesis by A39,A43,Th16;
end;
end;
A50: for n holds P[n] from NAT_1:sch 2(A29,A3);
ind T1+0<=i by XREAL_1:8;
hence thesis by A1,A2,A50;
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,TOPS_2:def 5;
A4: rng f=[#]T2 by A2,TOPS_2:def 5;
per cases;
suppose
A5: [#]T1={}T1;
then ind[#]T2=-1 by A4,Th6;
hence thesis by A4,A5,Def4,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 17;
A8: V2`c=A` by A6,SUBSET_1:31;
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:76
.=(([#]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:40;
then
A13: Cl V1 c=V2` by SUBSET_1:43;
Cl W1 c=Cl V1 by A10,PRE_TOPC:49;
then Cl W1 c=V2` by A13,XBOOLE_1:1;
then Cl W1 c=A` by A8,XBOOLE_1:1;
then
A14: A c=(Cl W1)` by SUBSET_1:35;
W1 c=Cl W1 by PRE_TOPC:48;
then
A15: (Cl W1)`misses W1 by SUBSET_1:44;
{p}c=W1 by A9,ZFMISC_1:37;
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:36,43;
take A1;
Cl A1 misses A2 by A23,TSEP_1:40;
then Cl A1\A2=Cl A1 by XBOOLE_1:83;
then Fr A1=Cl A1\A2\A1 by TOPS_1:76
.=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,XBOOLE_1:1,XXREAL_0:2 ,
ZFMISC_1:37;
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 B'=B as Subset of T|A by A2;
A5: B' is finite-ind by A1,A2,A4,Th4;
then ind B=ind B' 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 B'=B as Subset of T by A2;
B' is finite-ind by A2,A3,A10;
then ind B=ind B' by Th21;
hence thesis by A1,A2,A6,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 B'=B as Subset of T by A2;
A5: B' is finite-ind by A1,A2,A4,Th4;
then ind B=ind B' 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 B'=B as Subset of T|A by A2;
B' is finite-ind by A2,A3,A10;
then ind B=ind B' by Th22;
hence thesis by A1,A2,A6,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[set,set] 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 set st x in [:cT,TOP:]ex y be set st P[x,y]
proof
let x be set;
assume
x in [:cT,TOP:];
then consider p',A' be set such that
A4: p' in cT and
A5: A' in TOP and
A6: x=[p',A'] by ZFMISC_1:def 2;
reconsider p' as Point of T by A4;
reconsider A' as open Subset of T by A5,PRE_TOPC:def 5;
per cases;
suppose
A7: not p' in A';
take{}T;
let p be Point of T,A such that
A8: x=[p,A];
p=p' by A6,A8,ZFMISC_1:33;
hence thesis by A6,A7,A8,PRE_TOPC:def 5,ZFMISC_1:33;
end;
suppose
p' in A';
then consider W be open Subset of T such that
A9: p' in W & W c=A' 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=p' & A=A' by A6,ZFMISC_1:33;
hence thesis by A9,A10,PRE_TOPC:def 5;
end;
end;
consider f be Function such that
A11: dom f=[:cT,TOP:] and
A12: for x be set st x in [:cT,TOP:] holds P[x,f.x] from CLASSES1:sch
1(A3);
A13: rng f c=TOP
proof
let y be set;
assume
y in rng f;
then consider x be set such that
A14: x in dom f and
A15: f.x=y by FUNCT_1:def 5;
ex p,A be set 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 5;
let p be Point of T such that
A17: p in A;
A18: [p,A] in [:cT,TOP:] by A16,A17,ZFMISC_1:106;
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 5;
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 set such that
A20: x in dom f and
A21: f.x=B by FUNCT_1:def 5;
consider p,A be set such that
A22: p in cT and
A23: A in TOP and
A24: x=[p,A] by A11,A20,ZFMISC_1:def 2;
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:41;
0-1<=n-1 by XREAL_1:11;
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:78;
then reconsider W as open Subset of T by A30,PRE_TOPC:def 5;
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 A',B' be closed Subset of T st A' misses B' & A'\/B' = [#]T & A c= A' & B c=
B' 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 A',B' be
closed Subset of T st A' misses B' & A'\/B'=[#]T & A c=A' & B c=B';
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:37;
not p in U` by A3,XBOOLE_0:def 5;
then
A4: P misses U` by ZFMISC_1:56;
T is non empty by A3;
then consider A',B' be closed Subset of T such that
A5: A' misses B' and
A6: A'\/B'=[#]T and
A7: P c=A' and
A8: U`c=B' by A1,A4;
reconsider W=B'` as open Subset of T;
take W;
p in P by TARSKI:def 1;
then U``=U & not p in B' by A5,A7,XBOOLE_0:3;
hence p in W & W c=U by A3,A8,SUBSET_1:31,XBOOLE_0:def 5;
B'=A'` by A5,A6,PRE_TOPC:25;
then Fr B'={}T by TOPGEN_1:16;
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*