let T be 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 ) )
let n be Nat; ( ( 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 ) )
set TOP = the topology of T;
set cT = the carrier of T;
hereby ( 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 ) implies ( T is finite-ind & ind T <= n ) )
defpred S1[
object ,
object ]
means for
p being
Point of
T for
A being
Subset of
T st $1
= [p,A] holds
( $2
in the
topology of
T & ( not
p in A implies $2
= {} T ) & (
p in A implies ex
W being
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
;
ex RNG being Basis of T st
for B being Subset of T st B in RNG holds
( Fr b4 is finite-ind & ind (Fr b4) <= n - 1 )A3:
for
x being
object st
x in [: the carrier of T, the topology of T:] holds
ex
y being
object st
S1[
x,
y]
proof
let x be
object ;
( x in [: the carrier of T, the topology of T:] implies ex y being object st S1[x,y] )
assume
x in [: the carrier of T, the topology of T:]
;
ex y being object st S1[x,y]
then consider p9,
A9 being
object such that A4:
p9 in the
carrier of
T
and A5:
A9 in the
topology of
T
and A6:
x = [p9,A9]
by ZFMISC_1:def 2;
reconsider p9 =
p9 as
Point of
T by A4;
reconsider A9 =
A9 as
open Subset of
T by A5, PRE_TOPC:def 2;
per cases
( not p9 in A9 or p9 in A9 )
;
suppose A7:
not
p9 in A9
;
ex y being object st S1[x,y]take
{} T
;
S1[x, {} T]let p be
Point of
T;
for A being Subset of T st x = [p,A] holds
( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) )let A be
Subset of
T;
( x = [p,A] implies ( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) )assume A8:
x = [p,A]
;
( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) )
p = p9
by A6, A8, XTUPLE_0:1;
hence
(
{} T in the
topology of
T & ( not
p in A implies
{} T = {} T ) & (
p in A implies ex
W being
open Subset of
T st
(
W = {} T &
p in W &
W c= A &
ind (Fr W) <= n - 1 ) ) )
by A6, A7, A8, PRE_TOPC:def 2, XTUPLE_0:1;
verum end; end;
end; consider f being
Function such that A11:
dom f = [: the carrier of T, the topology of T:]
and A12:
for
x being
object st
x in [: the carrier of T, the topology of T:] holds
S1[
x,
f . x]
from CLASSES1:sch 1(A3);
A13:
rng f c= the
topology of
T
then reconsider RNG =
rng f as
Subset-Family of
T by XBOOLE_1:1;
then reconsider RNG =
RNG as
Basis of
T by A13, YELLOW_9:32;
take RNG =
RNG;
for B being Subset of T st B in RNG holds
( Fr b3 is finite-ind & ind (Fr b3) <= n - 1 )let B be
Subset of
T;
( B in RNG implies ( Fr b2 is finite-ind & ind (Fr b2) <= n - 1 ) )assume
B in RNG
;
( Fr b2 is finite-ind & ind (Fr b2) <= n - 1 )then consider x being
object such that A20:
x in dom f
and A21:
f . x = B
by FUNCT_1:def 3;
consider p,
A being
object such that A22:
p in the
carrier of
T
and A23:
A in the
topology of
T
and A24:
x = [p,A]
by A11, A20, ZFMISC_1:def 2;
reconsider A =
A as
set by TARSKI:1;
end;
given B being Basis of T such that A28:
for A being Subset of T st A in B holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 )
; ( T is finite-ind & ind T <= n )
then
T is finite-ind
by Th15;
hence
( T is finite-ind & ind T <= n )
by A29, Th16; verum