:: by Karol P\c{a}k

::

:: Received June 29, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

theorem Th1: :: TOPDIM_1:1

for T being TopSpace

for A, B being Subset of T

for F being Subset of (T | A) st F = B /\ A holds

Fr F c= (Fr B) /\ A

for A, B being Subset of T

for F being Subset of (T | A) st F = B /\ A holds

Fr F c= (Fr B) /\ A

proof end;

theorem Th2: :: TOPDIM_1:2

for T being TopSpace holds

( T is normal iff for A, B being closed Subset of T st A misses B holds

ex U, W being open Subset of T st

( A c= U & B c= W & Cl U misses Cl W ) )

( T is normal iff for A, B being closed Subset of T st A misses B holds

ex U, W being open Subset of T st

( A c= U & B c= W & Cl U misses Cl W ) )

proof end;

definition

let T be TopSpace;

ex b_{1} being SetSequence of (bool the carrier of T) st

for A being Subset of T

for n being Nat holds

( b_{1} . 0 = {({} T)} & ( not A in b_{1} . (n + 1) or A in b_{1} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{1} . n ) ) & ( ( A in b_{1} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{1} . n ) ) implies A in b_{1} . (n + 1) ) )

for b_{1}, b_{2} being SetSequence of (bool the carrier of T) st ( for A being Subset of T

for n being Nat holds

( b_{1} . 0 = {({} T)} & ( not A in b_{1} . (n + 1) or A in b_{1} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{1} . n ) ) & ( ( A in b_{1} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{1} . n ) ) implies A in b_{1} . (n + 1) ) ) ) & ( for A being Subset of T

for n being Nat holds

( b_{2} . 0 = {({} T)} & ( not A in b_{2} . (n + 1) or A in b_{2} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{2} . n ) ) & ( ( A in b_{2} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{2} . n ) ) implies A in b_{2} . (n + 1) ) ) ) holds

b_{1} = b_{2}

end;
func Seq_of_ind T -> SetSequence of (bool the carrier of T) means :Def1: :: TOPDIM_1:def 1

for A being Subset of T

for n being Nat holds

( it . 0 = {({} T)} & ( not A in it . (n + 1) or A in it . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in it . n ) ) & ( ( A in it . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in it . n ) ) implies A in it . (n + 1) ) );

existence for A being Subset of T

for n being Nat holds

( it . 0 = {({} T)} & ( not A in it . (n + 1) or A in it . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in it . n ) ) & ( ( A in it . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in it . n ) ) implies A in it . (n + 1) ) );

ex b

for A being Subset of T

for n being Nat holds

( b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

proof end;

uniqueness for b

for n being Nat holds

( b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

for n being Nat holds

( b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

b

proof end;

:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :

for T being TopSpace

for b_{2} being SetSequence of (bool the carrier of T) holds

( b_{2} = Seq_of_ind T iff for A being Subset of T

for n being Nat holds

( b_{2} . 0 = {({} T)} & ( not A in b_{2} . (n + 1) or A in b_{2} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{2} . n ) ) & ( ( A in b_{2} . n or for p being Point of (T | A)

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b_{2} . n ) ) implies A in b_{2} . (n + 1) ) ) );

for T being TopSpace

for b

( b

for n being Nat holds

( b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

for U being open Subset of (T | A) st p in U holds

ex W being open Subset of (T | A) st

( p in W & W c= U & Fr W in b

theorem Th3: :: TOPDIM_1:3

for T being TopSpace

for A, B being Subset of T

for n being Nat

for F being Subset of (T | A) st F = B holds

( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )

for A, B being Subset of T

for n being Nat

for F being Subset of (T | A) st F = B holds

( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )

proof end;

definition

let T be TopSpace;

let A be Subset of T;

end;
let A be Subset of T;

attr A is with_finite_small_inductive_dimension means :Def2: :: TOPDIM_1:def 2

ex n being Nat st A in (Seq_of_ind T) . n;

ex n being Nat st A in (Seq_of_ind T) . n;

:: deftheorem Def2 defines with_finite_small_inductive_dimension TOPDIM_1:def 2 :

for T being TopSpace

for A being Subset of T holds

( A is with_finite_small_inductive_dimension iff ex n being Nat st A in (Seq_of_ind T) . n );

for T being TopSpace

for A being Subset of T holds

( A is with_finite_small_inductive_dimension iff ex n being Nat st A in (Seq_of_ind T) . n );

notation

let T be TopSpace;

let A be Subset of T;

synonym finite-ind A for with_finite_small_inductive_dimension ;

end;
let A be Subset of T;

synonym finite-ind A for with_finite_small_inductive_dimension ;

definition

let T be TopSpace;

let G be Subset-Family of T;

end;
let G be Subset-Family of T;

attr G is with_finite_small_inductive_dimension means :: TOPDIM_1:def 3

ex n being Nat st G c= (Seq_of_ind T) . n;

ex n being Nat st G c= (Seq_of_ind T) . n;

:: deftheorem defines with_finite_small_inductive_dimension TOPDIM_1:def 3 :

for T being TopSpace

for G being Subset-Family of T holds

( G is with_finite_small_inductive_dimension iff ex n being Nat st G c= (Seq_of_ind T) . n );

for T being TopSpace

for G being Subset-Family of T holds

( G is with_finite_small_inductive_dimension iff ex n being Nat st G c= (Seq_of_ind T) . n );

notation

let T be TopSpace;

let G be Subset-Family of T;

synonym finite-ind G for with_finite_small_inductive_dimension ;

end;
let G be Subset-Family of T;

synonym finite-ind G for with_finite_small_inductive_dimension ;

theorem :: TOPDIM_1:4

for T being TopSpace

for A being Subset of T

for G being Subset-Family of T st A in G & G is finite-ind holds

A is finite-ind ;

for A being Subset of T

for G being Subset-Family of T st A in G & G is finite-ind holds

A is finite-ind ;

Lm1: for T being TopSpace

for A being finite Subset of T holds

( A is finite-ind & A in (Seq_of_ind T) . (card A) )

proof end;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is finite holds

b_{1} is finite-ind
by Lm1;

coherence

for b_{1} being Subset-Family of T st b_{1} is empty holds

b_{1} is finite-ind

ex b_{1} being Subset-Family of T st

( not b_{1} is empty & b_{1} is finite-ind )

end;
coherence

for b

b

coherence

for b

b

proof end;

existence ex b

( not b

proof end;

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is finite-ind )

end;
existence

ex b

( not b

proof end;

definition

let T be TopSpace;

end;
attr T is with_finite_small_inductive_dimension means :Def4: :: TOPDIM_1:def 4

[#] T is with_finite_small_inductive_dimension ;

[#] T is with_finite_small_inductive_dimension ;

:: deftheorem Def4 defines with_finite_small_inductive_dimension TOPDIM_1:def 4 :

for T being TopSpace holds

( T is with_finite_small_inductive_dimension iff [#] T is with_finite_small_inductive_dimension );

for T being TopSpace holds

( T is with_finite_small_inductive_dimension iff [#] T is with_finite_small_inductive_dimension );

Lm2: for X being set holds X in (Seq_of_ind (1TopSp X)) . 1

proof end;

registration
end;

registration
end;

definition

let T be TopSpace;

let A be Subset of T;

assume A1: A is finite-ind ;

ex b_{1} being Integer st

( A in (Seq_of_ind T) . (b_{1} + 1) & not A in (Seq_of_ind T) . b_{1} )

for b_{1}, b_{2} being Integer st A in (Seq_of_ind T) . (b_{1} + 1) & not A in (Seq_of_ind T) . b_{1} & A in (Seq_of_ind T) . (b_{2} + 1) & not A in (Seq_of_ind T) . b_{2} holds

b_{1} = b_{2}

end;
let A be Subset of T;

assume A1: A is finite-ind ;

func ind A -> Integer means :Def5: :: TOPDIM_1:def 5

( A in (Seq_of_ind T) . (it + 1) & not A in (Seq_of_ind T) . it );

existence ( A in (Seq_of_ind T) . (it + 1) & not A in (Seq_of_ind T) . it );

ex b

( A in (Seq_of_ind T) . (b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines ind TOPDIM_1:def 5 :

for T being TopSpace

for A being Subset of T st A is finite-ind holds

for b_{3} being Integer holds

( b_{3} = ind A iff ( A in (Seq_of_ind T) . (b_{3} + 1) & not A in (Seq_of_ind T) . b_{3} ) );

for T being TopSpace

for A being Subset of T st A is finite-ind holds

for b

( b

Lm3: for T being TopSpace

for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat

proof end;

registration

let T be non empty TopSpace;

let A be non empty finite-ind Subset of T;

coherence

ind A is natural

end;
let A be non empty finite-ind Subset of T;

coherence

ind A is natural

proof end;

theorem Th7: :: TOPDIM_1:7

for T being TopSpace

for n being Nat

for Af being finite-ind Subset of T holds

( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )

for n being Nat

for Af being finite-ind Subset of T holds

( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )

proof end;

theorem Th9: :: TOPDIM_1:9

for T being TopSpace

for n being Nat

for Af being finite-ind Subset of T holds

( ind Af <= n iff for p being Point of (T | Af)

for U being open Subset of (T | Af) st p in U holds

ex W being open Subset of (T | Af) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )

for n being Nat

for Af being finite-ind Subset of T holds

( ind Af <= n iff for p being Point of (T | Af)

for U being open Subset of (T | Af) st p in U holds

ex W being open Subset of (T | Af) st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )

proof end;

definition

let T be TopSpace;

let G be Subset-Family of T;

assume A1: G is finite-ind ;

ex b_{1} being Integer st

( G c= (Seq_of_ind T) . (b_{1} + 1) & - 1 <= b_{1} & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds

b_{1} <= i ) )

for b_{1}, b_{2} being Integer st G c= (Seq_of_ind T) . (b_{1} + 1) & - 1 <= b_{1} & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds

b_{1} <= i ) & G c= (Seq_of_ind T) . (b_{2} + 1) & - 1 <= b_{2} & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds

b_{2} <= i ) holds

b_{1} = b_{2}

end;
let G be Subset-Family of T;

assume A1: G is finite-ind ;

func ind G -> Integer means :Def6: :: TOPDIM_1:def 6

( G c= (Seq_of_ind T) . (it + 1) & - 1 <= it & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds

it <= i ) );

existence ( G c= (Seq_of_ind T) . (it + 1) & - 1 <= it & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds

it <= i ) );

ex b

( G c= (Seq_of_ind T) . (b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines ind TOPDIM_1:def 6 :

for T being TopSpace

for G being Subset-Family of T st G is finite-ind holds

for b_{3} being Integer holds

( b_{3} = ind G iff ( G c= (Seq_of_ind T) . (b_{3} + 1) & - 1 <= b_{3} & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds

b_{3} <= i ) ) );

for T being TopSpace

for G being Subset-Family of T st G is finite-ind holds

for b

( b

b

theorem :: TOPDIM_1:10

for T being TopSpace

for G being Subset-Family of T holds

( ( ind G = - 1 & G is finite-ind ) iff G c= {({} T)} )

for G being Subset-Family of T holds

( ( ind G = - 1 & G is finite-ind ) iff G c= {({} T)} )

proof end;

theorem Th11: :: TOPDIM_1:11

for T being TopSpace

for G being Subset-Family of T

for I being Integer holds

( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds

( A is finite-ind & ind A <= I ) ) ) )

for G being Subset-Family of T

for I being Integer holds

( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds

( A is finite-ind & ind A <= I ) ) ) )

proof end;

theorem :: TOPDIM_1:12

for T being TopSpace

for G1, G2 being Subset-Family of T st G1 is finite-ind & G2 c= G1 holds

( G2 is finite-ind & ind G2 <= ind G1 )

for G1, G2 being Subset-Family of T st G1 is finite-ind & G2 c= G1 holds

( G2 is finite-ind & ind G2 <= ind G1 )

proof end;

Lm4: for T being TopSpace

for G, G1 being Subset-Family of T

for i being 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 end;

registration

let T be TopSpace;

let G1, G2 be finite-ind Subset-Family of T;

coherence

for b_{1} being Subset-Family of T st b_{1} = G1 \/ G2 holds

b_{1} is with_finite_small_inductive_dimension

end;
let G1, G2 be finite-ind Subset-Family of T;

coherence

for b

b

proof end;

theorem :: TOPDIM_1:13

for T being TopSpace

for G, G1 being Subset-Family of T

for I being Integer st G is finite-ind & G1 is finite-ind & ind G <= I & ind G1 <= I holds

ind (G \/ G1) <= I by Lm4;

for G, G1 being Subset-Family of T

for I being Integer st G is finite-ind & G1 is finite-ind & ind G <= I & ind G1 <= I holds

ind (G \/ G1) <= I by Lm4;

theorem Th15: :: TOPDIM_1:15

for T being TopSpace st ex n being Nat st

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 & Fr W is finite-ind & ind (Fr W) <= n - 1 ) holds

T is finite-ind

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 & Fr W is finite-ind & ind (Fr W) <= n - 1 ) holds

T is finite-ind

proof end;

theorem Th16: :: TOPDIM_1:16

for n being Nat

for Tf being finite-ind TopSpace holds

( ind Tf <= n iff for p being Point of Tf

for U being open Subset of Tf st p in U holds

ex W being open Subset of Tf st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )

for Tf being finite-ind TopSpace holds

( ind Tf <= n iff for p being Point of Tf

for U being open Subset of Tf st p in U holds

ex W being open Subset of Tf st

( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )

proof end;

Lm5: for T being TopSpace

for Af being finite-ind Subset of T holds

( T | Af is finite-ind & ind (T | Af) = ind Af )

proof end;

Lm6: for Tf being finite-ind TopSpace

for A being Subset of Tf holds

( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )

proof end;

Lm7: for T being TopSpace

for A being Subset of T st T is finite-ind holds

A is finite-ind

proof end;

registration

let Tf be finite-ind TopSpace;

coherence

for b_{1} being Subset of Tf holds b_{1} is finite-ind
by Lm7;

end;
coherence

for b

registration

let T be TopSpace;

let Af be finite-ind Subset of T;

coherence

T | Af is with_finite_small_inductive_dimension by Lm5;

end;
let Af be finite-ind Subset of T;

coherence

T | Af is with_finite_small_inductive_dimension by Lm5;

:: Teoria wymiaru Th 1.1.2

theorem :: TOPDIM_1:17

theorem Th19: :: TOPDIM_1:19

for T being TopSpace

for A being Subset of T

for Af being finite-ind Subset of T st A c= Af holds

( A is finite-ind & ind A <= ind Af )

for A being Subset of T

for Af being finite-ind Subset of T st A c= Af holds

( A is finite-ind & ind A <= ind Af )

proof end;

theorem :: TOPDIM_1:20

theorem Th21: :: TOPDIM_1:21

for T being TopSpace

for A, B being Subset of T

for F being Subset of (T | A) st F = B & B is finite-ind holds

( F is finite-ind & ind F = ind B )

for A, B being Subset of T

for F being Subset of (T | A) st F = B & B is finite-ind holds

( F is finite-ind & ind F = ind B )

proof end;

theorem Th22: :: TOPDIM_1:22

for T being TopSpace

for A, B being Subset of T

for F being Subset of (T | A) st F = B & F is finite-ind holds

( B is finite-ind & ind F = ind B )

for A, B being Subset of T

for F being Subset of (T | A) st F = B & F is finite-ind holds

( B is finite-ind & ind F = ind B )

proof end;

Lm8: for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds

( T2 is finite-ind & ind T2 <= ind T1 )

proof end;

Lm9: for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds

( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )

proof end;

:: Teoria wymiaru Th 1.1.4

theorem :: TOPDIM_1:23

for n being Nat

for T being non empty TopSpace st T is regular holds

( ( T is finite-ind & ind T <= n ) iff for A being closed Subset of T

for p being Point of T st not p in A holds

ex L being Subset of T st

( L separates {p},A & L is finite-ind & ind L <= n - 1 ) )

for T being non empty TopSpace st T is regular holds

( ( T is finite-ind & ind T <= n ) iff for A being closed Subset of T

for p being Point of T st not p in A holds

ex L being Subset of T st

( L separates {p},A & L is finite-ind & ind L <= n - 1 ) )

proof end;

theorem :: TOPDIM_1:24

for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds

( T1 is finite-ind iff T2 is finite-ind ) by Lm9;

( T1 is finite-ind iff T2 is finite-ind ) by Lm9;

theorem :: TOPDIM_1:25

for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds

ind T1 = ind T2 by Lm9;

ind T1 = ind T2 by Lm9;

theorem Th26: :: TOPDIM_1:26

for T1, T2 being TopSpace

for A1 being Subset of T1

for A2 being Subset of T2 st A1,A2 are_homeomorphic holds

( A1 is finite-ind iff A2 is finite-ind )

for A1 being Subset of T1

for A2 being Subset of T2 st A1,A2 are_homeomorphic holds

( A1 is finite-ind iff A2 is finite-ind )

proof end;

theorem :: TOPDIM_1:27

for T1, T2 being TopSpace

for A1 being Subset of T1

for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds

ind A1 = ind A2

for A1 being Subset of T1

for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is finite-ind holds

ind A1 = ind A2

proof end;

theorem :: TOPDIM_1:28

for T1, T2 being TopSpace st [:T1,T2:] is finite-ind holds

( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] )

( [:T2,T1:] is finite-ind & ind [:T1,T2:] = ind [:T2,T1:] )

proof end;

theorem :: TOPDIM_1:29

for T being TopSpace

for A being Subset of T

for G being Subset-Family of T

for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds

( G is finite-ind & ind G = ind Ga )

for A being Subset of T

for G being Subset-Family of T

for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds

( G is finite-ind & ind G = ind Ga )

proof end;

theorem :: TOPDIM_1:30

for T being TopSpace

for A being Subset of T

for G being Subset-Family of T

for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds

( Ga is finite-ind & ind G = ind Ga )

for A being Subset of T

for G being Subset-Family of T

for Ga being Subset-Family of (T | A) st G is finite-ind & Ga = G holds

( Ga is finite-ind & ind G = ind Ga )

proof end;

:: Teoria wymiaru Th 1.1.6

theorem Th31: :: TOPDIM_1:31

for T being TopSpace

for n being Nat holds

( ( T is finite-ind & ind T <= n ) iff ex Bas being Basis of T st

for A being Subset of T st A in Bas holds

( Fr A is finite-ind & ind (Fr A) <= n - 1 ) )

for n being Nat holds

( ( T is finite-ind & ind T <= n ) iff ex Bas being Basis of T st

for A being Subset of T st A in Bas holds

( Fr A is finite-ind & ind (Fr A) <= n - 1 ) )

proof end;

:: Wprowadzenie do topologi 3.4.2 "=>"

theorem Th32: :: TOPDIM_1:32

for T being TopSpace st T is T_1 & ( for A, B being closed Subset of T st A misses B holds

ex A9, B9 being 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 )

ex A9, B9 being 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 end;

theorem Th33: :: TOPDIM_1:33

for X being set

for f being SetSequence of X ex g being SetSequence of X st

( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds

g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st

( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )

for f being SetSequence of X ex g being SetSequence of X st

( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds

g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st

( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )

proof end;

:: Wprowadzenie do topologi 3.4.2 "<="

theorem Th34: :: TOPDIM_1:34

for T being TopSpace st T is finite-ind & ind T <= 0 & T is Lindelof holds

for A, B being closed Subset of T st A misses B holds

ex A9, B9 being closed Subset of T st

( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )

for A, B being closed Subset of T st A misses B holds

ex A9, B9 being closed Subset of T st

( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )

proof end;

:: Teoria wymiaru Th 1.2.6

theorem Th35: :: TOPDIM_1:35

for T being TopSpace st T is T_1 & T is Lindelof holds

( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds

{} T separates A,B )

( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds

{} T separates A,B )

proof end;

theorem :: TOPDIM_1:36

for T being TopSpace st T is T_4 & T is Lindelof & 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 <= 0 ) holds

( T is finite-ind & ind T <= 0 )

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= 0 ) holds

( T is finite-ind & ind T <= 0 )

proof end;

:: Teoria wymiaru Th 1.2.11

theorem Th37: :: TOPDIM_1:37

for TM being metrizable TopSpace

for A, B being closed Subset of TM st A misses B holds

for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds

ex L being Subset of TM st

( L separates A,B & L misses Null )

for A, B being closed Subset of TM st A misses B holds

for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds

ex L being Subset of TM st

( L separates A,B & L misses Null )

proof end;

:: Teoria wymiaru Th 1.2.12

theorem Th38: :: TOPDIM_1:38

for TM being metrizable TopSpace

for Null being Subset of TM st TM | Null is second-countable holds

( ( Null is finite-ind & ind Null <= 0 ) 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 & Null misses Fr W ) )

for Null being Subset of TM st TM | Null is second-countable holds

( ( Null is finite-ind & ind Null <= 0 ) 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 & Null misses Fr W ) )

proof end;

:: Teoria wymiaru Th 1.2.13

theorem Th39: :: TOPDIM_1:39

for TM being metrizable TopSpace

for Null being Subset of TM st TM | Null is second-countable holds

( ( Null is finite-ind & ind Null <= 0 ) iff ex B being Basis of TM st

for A being Subset of TM st A in B holds

Null misses Fr A )

for Null being Subset of TM st TM | Null is second-countable holds

( ( Null is finite-ind & ind Null <= 0 ) iff ex B being Basis of TM st

for A being Subset of TM st A in B holds

Null misses Fr A )

proof end;

:: Teoria wymiaru Th 1.5.2

theorem :: TOPDIM_1:40

for TM being metrizable TopSpace

for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds

( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )

for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds

( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )

proof end;

:: with limited small inductive dimension