set TOP = the topology of TM;
set cTM = the carrier of TM;
let Am be Subset of TM; ( Am is open implies Am is F_sigma )
assume A1:
Am is open
; Am is F_sigma
per cases
( TM is empty or not TM is empty )
;
suppose A3:
not
TM is
empty
;
Am is F_sigma per cases
( Am = [#] TM or Am <> [#] TM )
;
suppose A4:
Am <> [#] TM
;
Am is F_sigma consider metr being
Function of
[: the carrier of TM, the carrier of TM:],
REAL such that A5:
metr is_metric_of the
carrier of
TM
and A6:
Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the
topology of
TM
by PCOMPS_1:def 8;
reconsider Tm =
SpaceMetr ( the
carrier of
TM,
metr) as non
empty MetrSpace by A3, A5, PCOMPS_1:36;
set TTm =
TopSpaceMetr Tm;
Am in the
topology of
(TopSpaceMetr Tm)
by A1, A6;
then reconsider a =
Am as
open Subset of
(TopSpaceMetr Tm) by PRE_TOPC:def 2;
({} (TopSpaceMetr Tm)) ` = [#] (TopSpaceMetr Tm)
;
then reconsider A9 =
a ` as non
empty closed Subset of
(TopSpaceMetr Tm) by A3, A4, A5, PCOMPS_2:4;
defpred S1[
object ,
object ]
means for
n being
Nat st
n = TM holds
c2 = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } ;
A7:
for
x being
object st
x in NAT holds
ex
y being
object st
(
y in the
topology of
TM &
S1[
x,
y] )
consider p being
sequence of the
topology of
TM such that A8:
for
x being
object st
x in NAT holds
S1[
x,
p . x]
from FUNCT_2:sch 1(A7);
reconsider RNG =
rng p as
open Subset-Family of
TM by TOPS_2:11, XBOOLE_1:1;
set Crng =
COMPLEMENT RNG;
A9:
dom p = NAT
by FUNCT_2:def 1;
A10:
[#] TM = [#] (TopSpaceMetr Tm)
by A3, A5, PCOMPS_2:4;
A11:
union (COMPLEMENT RNG) = Am
proof
let x be
object ;
TARSKI:def 3 ( not x in Am or x in union (COMPLEMENT RNG) )
assume A18:
x in Am
;
x in union (COMPLEMENT RNG)
then reconsider q =
x as
Point of
(TopSpaceMetr Tm) by A3, A5, PCOMPS_2:4;
(
Cl A9 = A9 & not
q in A9 )
by A18, PRE_TOPC:22, XBOOLE_0:def 5;
then A19:
(dist_min A9) . q <> 0
by HAUSDORF:8;
(dist_min A9) . q >= 0
by JORDAN1K:9;
then consider n being
Nat such that A20:
1
/ (2 |^ n) <= (dist_min A9) . q
by A19, PREPOWER:92;
A21:
n in NAT
by ORDINAL1:def 12;
p . n in RNG
by A9, FUNCT_1:def 3, A21;
then reconsider pn =
p . n as
Subset of
TM ;
A22:
pn = { s where s is Point of (TopSpaceMetr Tm) : (dist_min A9) . s < 1 / (2 |^ n) }
by A8, A21;
for
s being
Point of
(TopSpaceMetr Tm) st
s = q holds
not 1
/ (2 |^ n) > (dist_min A9) . s
by A20;
then
not
q in pn
by A22;
then A23:
q in pn `
by A18, XBOOLE_0:def 5;
(pn `) ` in RNG
by A9, FUNCT_1:def 3, A21;
then
pn ` in COMPLEMENT RNG
by SETFAM_1:def 7;
hence
x in union (COMPLEMENT RNG)
by A23, TARSKI:def 4;
verum
end;
(
COMPLEMENT RNG is
closed &
RNG is
countable )
by A9, CARD_3:93, TOPS_2:10;
hence
Am is
F_sigma
by A11, TOPGEN_4:def 6;
verum end; end; end; end;