let n be Nat; ( TOP-REAL n is with_finite_small_inductive_dimension & ind (TOP-REAL n) <= n )
defpred S1[ Nat] means ( TOP-REAL $1 is with_finite_small_inductive_dimension & ind (TOP-REAL $1) <= $1 );
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
F:
(
TopStruct(# the
carrier of
(TOP-REAL n),the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n) &
TopStruct(# the
carrier of
(TOP-REAL (n + 1)),the
topology of
(TOP-REAL (n + 1)) #)
= TopSpaceMetr (Euclid (n + 1)) &
TopStruct(# the
carrier of
(TOP-REAL 1),the
topology of
(TOP-REAL 1) #)
= TopSpaceMetr (Euclid 1) )
by EUCLID:def 8;
A2:
n in NAT
by ORDINAL1:def 13;
then A3:
[:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):],
TopSpaceMetr (Euclid (n + 1)) are_homeomorphic
by TOPREAL7:27;
TOP-REAL 1,
TopSpaceMetr (Euclid 1) are_homeomorphic
by F, YELLOW14:20;
then X1:
(
TopSpaceMetr (Euclid 1) is
with_finite_small_inductive_dimension &
ind (TopSpaceMetr (Euclid 1)) = 1 )
by Lm7, TOPDIM_1:24, TOPDIM_1:25;
assume A4:
S1[
n]
;
S1[n + 1]
P0:
TOP-REAL n,
TopSpaceMetr (Euclid n) are_homeomorphic
by F, YELLOW14:20;
P1:
TOP-REAL (n + 1),
TopSpaceMetr (Euclid (n + 1)) are_homeomorphic
by F, YELLOW14:20;
X2:
(
TopSpaceMetr (Euclid n) is
with_finite_small_inductive_dimension &
ind (TopSpaceMetr (Euclid n)) = ind (TOP-REAL n) )
by A4, TOPDIM_1:24, TOPDIM_1:25, P0;
A5:
ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= (ind (TopSpaceMetr (Euclid n))) + 1
by X2, Lm5, F, X1;
(ind (TopSpaceMetr (Euclid n))) + 1
<= n + 1
by XREAL_1:8, A4, X2;
then aa:
ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= n + 1
by A5, XXREAL_0:2;
ab:
ind (TopSpaceMetr (Euclid (n + 1))) <= n + 1
by aa, A2, TOPREAL7:27, TOPDIM_1:25, X2, X1, F;
TopSpaceMetr (Euclid (n + 1)) is
with_finite_small_inductive_dimension
by X2, X1, F, A3, TOPDIM_1:24;
then
TOP-REAL (n + 1) is
with_finite_small_inductive_dimension
by TOPDIM_1:24, P1;
hence
S1[
n + 1]
by ab, F, YELLOW14:20, TOPDIM_1:25;
verum
end;
A6:
S1[ 0 ]
by Lm6;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A1);
hence
( TOP-REAL n is with_finite_small_inductive_dimension & ind (TOP-REAL n) <= n )
; verum