let T be TopSpace; ( T is finite-ind & ind T <= 0 & T is Lindelof implies for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) )
assume that
A1:
( T is finite-ind & ind T <= 0 )
and
A2:
T is Lindelof
; for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
set CT = [#] T;
let A, B be closed Subset of T; ( A misses B implies ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) )
assume A3:
A misses B
; ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
per cases
( [#] T = {} or [#] T <> {} )
;
suppose A5:
[#] T <> {}
;
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )defpred S1[
object ,
object ]
means ex
D2 being
set st
(
D2 = $2 & $1 is
Point of
T & $1
in D2 & $2 is
open closed Subset of
T & (
D2 c= A ` or
D2 c= B ` ) );
A6:
for
x being
object st
x in [#] T holds
ex
y being
object st
(
y in bool ([#] T) &
S1[
x,
y] )
proof
let x be
object ;
( x in [#] T implies ex y being object st
( y in bool ([#] T) & S1[x,y] ) )
assume A7:
x in [#] T
;
ex y being object st
( y in bool ([#] T) & S1[x,y] )
reconsider p =
x as
Point of
T by A7;
per cases
( p in A ` or not p in A ` )
;
suppose A11:
not
p in A `
;
ex y being object st
( y in bool ([#] T) & S1[x,y] )A12:
A c= B `
by A3, SUBSET_1:23;
p in A
by A7, A11, XBOOLE_0:def 5;
then consider W being
open Subset of
T such that A13:
(
p in W &
W c= B ` )
and A14:
Fr W is
finite-ind
and A15:
ind (Fr W) <= 0 - 1
by A1, A12, Th16;
take
W
;
( W in bool ([#] T) & S1[x,W] )thus
W in bool ([#] T)
;
S1[x,W]take
W
;
( W = W & x is Point of T & x in W & W is open closed Subset of T & ( W c= A ` or W c= B ` ) )
- 1
<= ind (Fr W)
by A14, Th5;
then
ind (Fr W) = - 1
by A15, XXREAL_0:1;
then
Fr W = {} T
by A14, Th6;
hence
(
W = W &
x is
Point of
T &
x in W &
W is
open closed Subset of
T & (
W c= A ` or
W c= B ` ) )
by A13, TOPGEN_1:14;
verum end; end;
end; consider F being
Function of
([#] T),
(bool ([#] T)) such that A16:
for
x being
object st
x in [#] T holds
S1[
x,
F . x]
from FUNCT_2:sch 1(A6);
reconsider RNG =
rng F as
Subset-Family of
T ;
A17:
dom F = [#] T
by FUNCT_2:def 1;
[#] T c= union RNG
then
[#] T = union RNG
;
then A19:
RNG is
Cover of
T
by SETFAM_1:45;
RNG is
open
then consider G being
Subset-Family of
T such that A21:
G c= RNG
and A22:
G is
Cover of
T
and A23:
G is
countable
by A2, A19, METRIZTS:def 2;
not
T is
empty
by A5;
then A24:
not
G is
empty
by A22, TOPS_2:3;
then consider U being
sequence of
G such that A25:
rng U = G
by A23, CARD_3:96;
A26:
dom U = NAT
by A24, FUNCT_2:def 1;
then reconsider U =
U as
SetSequence of
([#] T) by A25, FUNCT_2:2;
consider V being
SetSequence of
([#] T) such that A27:
union (rng U) = union (rng V)
and A28:
for
i,
j being
Nat st
i <> j holds
V . i misses V . j
and A29:
for
n being
Nat ex
Un being
finite Subset-Family of
([#] T) st
(
Un = { (U . i) where i is Element of NAT : i < n } &
V . n = (U . n) \ (union Un) )
by Th33;
reconsider rngV =
rng V as
Subset-Family of
T ;
set AA =
{ (V . n) where n is Element of NAT : V . n misses B } ;
A30:
{ (V . n) where n is Element of NAT : V . n misses B } c= rng V
then reconsider AA =
{ (V . n) where n is Element of NAT : V . n misses B } as
Subset-Family of
T by XBOOLE_1:1;
set BB =
rngV \ AA;
A31:
rngV is
open
then
union AA is
open
by A30, TOPS_2:11, TOPS_2:19;
then reconsider UAA =
union AA,
UBB =
union (rngV \ AA) as
open Subset of
T by A31, TOPS_2:15, TOPS_2:19;
A38:
UAA misses UBB
rngV = (rngV \ AA) \/ AA
by A30, XBOOLE_1:45;
then A49:
UAA \/ UBB =
union G
by A25, A27, ZFMISC_1:78
.=
[#] T
by A22, SETFAM_1:45
;
then A50:
UAA = UBB `
by A38, PRE_TOPC:5;
B misses UAA
then A55:
B c= UAA `
by SUBSET_1:23;
A misses UBB
proof
assume
A meets UBB
;
contradiction
then consider x being
object such that A56:
x in A
and A57:
x in union (rngV \ AA)
by XBOOLE_0:3;
consider Bx being
set such that A58:
x in Bx
and A59:
Bx in rngV \ AA
by A57, TARSKI:def 4;
Bx in rngV
by A59, XBOOLE_0:def 5;
then consider m being
object such that A60:
m in dom V
and A61:
V . m = Bx
by FUNCT_1:def 3;
reconsider m =
m as
Element of
NAT by A60;
not
V . m in AA
by A59, A61, XBOOLE_0:def 5;
then
V . m meets B
;
then consider b being
object such that A62:
b in V . m
and A63:
b in B
by XBOOLE_0:3;
U . m in rng U
by A26, FUNCT_1:def 3;
then consider p being
object such that A64:
p in dom F
and A65:
F . p = U . m
by A21, A25, FUNCT_1:def 3;
reconsider Fp =
F . p as
Subset of
T by A65;
A66:
ex
Un being
finite Subset of
(bool ([#] T)) st
(
Un = { (U . i) where i is Element of NAT : i < m } &
V . m = (U . m) \ (union Un) )
by A29;
then
b in U . m
by A62, XBOOLE_0:def 5;
then
Fp meets B
by A63, A65, XBOOLE_0:3;
then A67:
not
Fp c= B `
by SUBSET_1:23;
S1[
p,
F . p]
by A16, A64;
then A68:
U . m c= A `
by A65, A67;
x in U . m
by A58, A61, A66, XBOOLE_0:def 5;
hence
contradiction
by A56, A68, XBOOLE_0:def 5;
verum
end; then
A c= UAA
by A50, SUBSET_1:23;
hence
ex
A9,
B9 being
closed Subset of
T st
(
A9 misses B9 &
A9 \/ B9 = [#] T &
A c= A9 &
B c= B9 )
by A38, A49, A50, A55;
verum end; end;