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 finite-ind & 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 finite-ind & 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 finite-ind & 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 finite-ind & ind (Fr W) <= 1 - 1 )
reconsider p9 =
p as
Point of
(Euclid 1) by Lm6;
set M =
Euclid 1;
A3:
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 A3, PRE_TOPC:30;
then consider r being
Real such that A4:
r > 0
and A5:
Ball (
p9,
r)
c= U
by A2, TOPMETR:15;
reconsider B =
Ball (
p9,
r) as
open Subset of
(TOP-REAL 1) by KURATO_2:1;
take
B
;
( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 )
p9 is
Tuple of 1,
REAL
by FINSEQ_2:131;
then consider p1 being
Element of
REAL such that A6:
p9 = <*p1*>
by FINSEQ_2:97;
A7:
Ball (
p,
r)
= Ball (
p9,
r)
by TOPREAL9:13;
then A8:
Fr B = {<*(p1 - r)*>,<*(p1 + r)*>}
by A4, A6, Th18;
TOP-REAL 1 is
metrizable
by A3, PCOMPS_1:def 8;
then
(TOP-REAL 1) | (Fr B) is
metrizable
;
hence
(
p in B &
B c= U &
Fr B is
finite-ind &
ind (Fr B) <= 1
- 1 )
by A4, A5, A7, Th19, A8, JORDAN:16;
verum
end;
then A9:
TOP-REAL 1 is finite-ind
by TOPDIM_1:15;
A10:
ind (TOP-REAL 1) >= 1
proof
reconsider jj = 1 as
Element of
REAL by XREAL_0:def 1;
reconsider p =
<*(In (0,REAL))*>,
q =
<*jj*> as
Point of
(Euclid 1) by FINSEQ_2:98;
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) ;
A11:
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:1;
assume
ind (TOP-REAL 1) < 1
;
contradiction
then
ind (TOP-REAL 1) < 1
+ 0
;
then A12:
ind (TOP-REAL 1) <= 0
by INT_1:7;
p in B
by JORDAN:16;
then consider W being
open Subset of
(TOP-REAL 1) such that A13:
p in W
and A14:
W c= B
and A15:
(
Fr W is
finite-ind &
ind (Fr W) <= 0 - 1 )
by A9, A12, TOPDIM_1:16;
Fr W = {} (TOP-REAL 1)
by A15;
then A16:
W is
closed
by TOPGEN_1:14;
A17:
W \/ (W `) = [#] (TOP-REAL 1)
by PRE_TOPC:2;
W misses W `
by SUBSET_1:24;
then
(
[#] (TOP-REAL 1) is
convex &
W,
W ` are_separated )
by A16, CONNSP_1:2;
then A18:
W ` = {} (TOP-REAL 1)
by A13, A17, CONNSP_1:15;
A19:
B = { <*s*> where s is Real : ( 0 - 1 < s & s < 0 + 1 ) }
by A11, JORDAN2B:27;
A20:
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 A14;
hence
contradiction
by A20, A18, XBOOLE_0:def 5;
verum
end;
ind (TOP-REAL 1) <= 1
by A1, A9, TOPDIM_1:16;
hence
( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 )
by A1, A10, TOPDIM_1:15, XXREAL_0:1; verum