set T = TOP-REAL 1;
A1:
for p being Point of (TOP-REAL 1)
for U being open Subset of (TOP-REAL 1) st p in U holds
ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 1 - 1 )
proof
let p be
Point of
(TOP-REAL 1);
for U being open Subset of (TOP-REAL 1) st p in U holds
ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 1 - 1 )let U be
open Subset of
(TOP-REAL 1);
( p in U implies ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 1 - 1 ) )
assume A2:
p in U
;
ex W being open Subset of (TOP-REAL 1) st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 1 - 1 )
reconsider p9 =
p as
Point of
(Euclid 1) by A;
set M =
Euclid 1;
B1:
TopStruct(# the
carrier of
(TopSpaceMetr (Euclid 1)),the
topology of
(TopSpaceMetr (Euclid 1)) #)
= TopStruct(# the
carrier of
(TOP-REAL 1),the
topology of
(TOP-REAL 1) #)
by EUCLID:def 8;
then reconsider V =
U as
Subset of
(TopSpaceMetr (Euclid 1)) ;
V is
open
by B1, PRE_TOPC:60;
then consider r being
real number such that A3:
r > 0
and A4:
Ball p9,
r c= U
by A2, TOPMETR:22;
reconsider B =
Ball p9,
r as
open Subset of
(TOP-REAL 1) by KURATO_2:30;
take
B
;
( p in B & B c= U & Fr B is with_finite_small_inductive_dimension & ind (Fr B) <= 1 - 1 )
p9 is
Tuple of 1,
REAL
by FINSEQ_2:151;
then consider p1 being
Real such that A5:
p9 = <*p1*>
by FINSEQ_2:117;
A6:
Ball p,
r = Ball p9,
r
by TOPREAL9:13;
then Aa:
Fr B = {<*(p1 - r)*>,<*(p1 + r)*>}
by A3, A5, Th18;
TOP-REAL 1 is
metrizable
then
(TOP-REAL 1) | (Fr B) is
metrizable
;
hence
(
p in B &
B c= U &
Fr B is
with_finite_small_inductive_dimension &
ind (Fr B) <= 1
- 1 )
by A3, A4, A6, Th19, JORDAN:16, Aa;
verum
end;
then A7:
TOP-REAL 1 is with_finite_small_inductive_dimension
by TOPDIM_1:15;
A8:
ind (TOP-REAL 1) >= 1
proof
reconsider p =
<*0 *>,
q =
<*1*> as
Point of
(Euclid 1) by FINSEQ_2:118;
TopStruct(# the
carrier of
(TOP-REAL 1),the
topology of
(TOP-REAL 1) #)
= TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
then reconsider p9 =
p as
Point of
(TOP-REAL 1) ;
A9:
Ball p,1
= Ball p9,1
by TOPREAL9:13;
then reconsider B =
Ball p9,1 as
open Subset of
(TOP-REAL 1) by KURATO_2:30;
assume
ind (TOP-REAL 1) < 1
;
contradiction
then
ind (TOP-REAL 1) < 1
+ 0
;
then A10:
ind (TOP-REAL 1) <= 0
by INT_1:20;
p in B
by JORDAN:16;
then consider W being
open Subset of
(TOP-REAL 1) such that A11:
p in W
and A12:
W c= B
and A13:
(
Fr W is
with_finite_small_inductive_dimension &
ind (Fr W) <= 0 - 1 )
by A7, A10, TOPDIM_1:16;
Fr W = {} (TOP-REAL 1)
by A13;
then A14:
W is
closed
by TOPGEN_1:16;
A15:
W \/ (W ` ) = [#] (TOP-REAL 1)
by PRE_TOPC:18;
W misses W `
by SUBSET_1:44;
then
(
[#] (TOP-REAL 1) is
connected &
W,
W ` are_separated )
by A14, A15, CONNSP_1:3, JORDAN2C:22;
then A16:
W ` = {} (TOP-REAL 1)
by A11, A15, CONNSP_1:16;
A17:
B = { <*s*> where s is Real : ( 0 - 1 < s & s < 0 + 1 ) }
by A9, JORDAN2B:33;
A:
TopStruct(# the
carrier of
(TOP-REAL 1),the
topology of
(TOP-REAL 1) #)
= TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
not
q in B
then
not
q in W
by A12;
hence
contradiction
by A, A16, XBOOLE_0:def 5;
verum
end;
ind (TOP-REAL 1) <= 1
by A1, A7, TOPDIM_1:16;
hence
( TOP-REAL 1 is with_finite_small_inductive_dimension & ind (TOP-REAL 1) = 1 )
by A1, A8, TOPDIM_1:15, XXREAL_0:1; verum