defpred S1[ Nat] means for T being TopSpace
for A being finite Subset of T st card A <= $1 holds
( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) );
let T be TopSpace; :: thesis: for A being finite Subset of T holds
( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; :: thesis: ( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
:: thesis: S1[n + 1]
let T be
TopSpace;
:: thesis: for A being finite Subset of T st card A <= n + 1 holds
( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )let A be
finite Subset of
T;
:: thesis: ( card A <= n + 1 implies ( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) ) )
assume A3:
card A <= n + 1
;
:: thesis: ( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )
per cases
( card A <= n or card A = n + 1 )
by A3, NAT_1:8;
suppose A4:
card A = n + 1
;
:: thesis: ( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )
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 (Seq_of_ind T) . n )
proof
let p be
Point of
(T | A);
:: thesis: 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 (Seq_of_ind T) . n )let U be
open Subset of
(T | A);
:: thesis: ( p in U implies ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume A5:
p in U
;
:: thesis: ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
take W =
U;
:: thesis: ( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
{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;
:: thesis: Fr W in (Seq_of_ind T) . n
[#] (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< A
by A7, XBOOLE_0:def 8;
(Cl W) \ W c= A \ W
by A8, XBOOLE_1:33;
then
card (Fr W) <= card (A \ {p})
by A6, NAT_1:44, XBOOLE_1:1;
then
card (Fr W) < n + 1
by A4, A9, CARD_2:67, XXREAL_0:2;
then A10:
card (Fr W) <= n
by NAT_1:13;
then A11:
Fr W in (Seq_of_ind (T | A)) . (card (Fr W))
by A2;
n in NAT
by ORDINAL1:def 13;
then
(Seq_of_ind (T | A)) . (card (Fr W)) c= (Seq_of_ind (T | A)) . n
by A10, PROB_1:def 7;
then
FrW in (Seq_of_ind T) . n
by A11, Th3;
hence
Fr W in (Seq_of_ind T) . n
;
:: thesis: verum
end; then
A in (Seq_of_ind T) . (card A)
by A4, Def1;
hence
(
A is
with_finite_small_inductive_dimension &
A in (Seq_of_ind T) . (card A) )
by Def2;
:: thesis: verum
end;
A12:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A12, A1);
then
S1[ card A]
;
hence
( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )
; :: thesis: verum