:: Small {I}nductive {D}imension of {T}opological {S}paces
:: by Karol P\c{a}k
::
:: Received June 29, 2009
:: Copyright (c) 2009-2016 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;
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 :: TOPDIM_1:1
F = B/\A implies Fr F c= Fr B/\A;
theorem :: TOPDIM_1:2
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;
:: 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
:: TOPDIM_1:def 1
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);
end;
registration
let T;
cluster Seq_of_ind T -> non-descending;
end;
theorem :: TOPDIM_1:3
for F st F = B holds F in (Seq_of_ind T|A).n iff B in (Seq_of_ind T).n;
definition
let T,A;
attr A is with_finite_small_inductive_dimension means
:: TOPDIM_1:def 2
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
:: TOPDIM_1:def 3
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 :: TOPDIM_1:4
A in G & G is finite-ind implies A is finite-ind;
registration
let T;
cluster finite -> finite-ind for Subset of T;
cluster empty -> finite-ind for Subset-Family of T;
cluster non empty finite-ind for Subset-Family of T;
end;
registration
let T be non empty TopSpace;
cluster non empty finite-ind for Subset of T;
end;
definition
let T;
attr T is with_finite_small_inductive_dimension means
:: TOPDIM_1:def 4
[#]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;
end;
registration
let X be set;
cluster 1TopSp X -> finite-ind;
end;
registration
cluster non empty finite-ind for TopSpace;
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
A is finite-ind;
func ind A -> Integer means
:: TOPDIM_1:def 5
A in (Seq_of_ind T).(it+1) & not A in ( Seq_of_ind T).it;
end;
theorem :: TOPDIM_1:5
-1 <= ind Af;
theorem :: TOPDIM_1:6
ind Af = -1 iff Af is empty;
registration
let T be non empty TopSpace;
let A be non empty finite-ind Subset of T;
cluster ind A -> natural;
end;
theorem :: TOPDIM_1:7
ind Af <= n-1 iff Af in (Seq_of_ind T).n;
theorem :: TOPDIM_1:8
for A be finite Subset of T holds ind A < card A;
theorem :: TOPDIM_1:9
ind Af <= n iff for p be Point of T|Af,U be open Subset of T|Af
st p in U ex W be open Subset of T|Af st p in W & W c= U & Fr W is finite-ind &
ind Fr W <= n-1;
definition
let T;
let G such that
G is finite-ind;
func ind G -> Integer means
:: TOPDIM_1:def 6
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;
end;
theorem :: TOPDIM_1:10
ind G = -1 & G is finite-ind iff G c= {{}T};
theorem :: TOPDIM_1:11
G is finite-ind & ind G <= I iff -1 <= I & for A st A in G holds
A is finite-ind & ind A <= I;
theorem :: TOPDIM_1:12
G1 is finite-ind & G2 c= G1 implies G2 is finite-ind & ind G2 <= ind G1;
registration
let T;
let G1,G2 be finite-ind Subset-Family of T;
cluster G1 \/ G2 -> finite-ind for Subset-Family of T;
end;
theorem :: TOPDIM_1:13
G is finite-ind & G1 is finite-ind & ind G <= I & ind G1 <= I implies
ind (G\/G1) <= I;
definition
let T;
func ind T -> Integer equals
:: TOPDIM_1:def 7
ind [#]T;
end;
registration
let T be non empty finite-ind TopSpace;
cluster ind T -> natural;
end;
theorem :: TOPDIM_1:14
for X be non empty set holds ind 1TopSp X = 0;
theorem :: TOPDIM_1:15
(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;
theorem :: TOPDIM_1:16
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;
begin :: Monotonic of the Small Inductive Dimension
registration
let Tf;
cluster -> finite-ind for Subset of Tf;
end;
registration
let T,Af;
cluster T|Af -> finite-ind;
end;
:: Teoria wymiaru Th 1.1.2
theorem :: TOPDIM_1:17
ind T|Af = ind Af;
theorem :: TOPDIM_1:18
T|A is finite-ind implies A is finite-ind;
theorem :: TOPDIM_1:19
A c= Af implies A is finite-ind & ind A <= ind Af;
theorem :: TOPDIM_1:20
for A be Subset of Tf holds ind A <= ind Tf;
theorem :: TOPDIM_1:21
F = B & B is finite-ind implies F is finite-ind & ind F = ind B;
theorem :: TOPDIM_1:22
F = B & F is finite-ind implies B is finite-ind & ind F = ind B;
:: Teoria wymiaru Th 1.1.4
theorem :: TOPDIM_1:23
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;
theorem :: TOPDIM_1:24
T1,T2 are_homeomorphic implies (T1 is finite-ind iff T2 is finite-ind);
theorem :: TOPDIM_1:25
T1,T2 are_homeomorphic & T1 is finite-ind implies ind T1 = ind T2;
theorem :: TOPDIM_1:26
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;
theorem :: TOPDIM_1:27
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;
theorem :: TOPDIM_1:28
[:T1,T2:] is finite-ind implies [:T2,T1:] is finite-ind & ind [:T1,T2
:] = ind [:T2,T1:];
theorem :: TOPDIM_1:29
for Ga be Subset-Family of T|A st Ga is finite-ind & Ga = G holds G is
finite-ind & ind G = ind Ga;
theorem :: TOPDIM_1:30
for Ga be Subset-Family of T|A st G is finite-ind & Ga = G holds Ga is
finite-ind & ind G = ind Ga;
begin :: Basic Properties for zero dimensional Topological Spaces
:: Teoria wymiaru Th 1.1.6
theorem :: TOPDIM_1:31
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;
:: Wprowadzenie do topologi 3.4.2 "=>"
theorem :: TOPDIM_1:32
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;
theorem :: TOPDIM_1:33
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:i