let T be TopSpace; ( T is with_finite_small_inductive_dimension & 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 with_finite_small_inductive_dimension & 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[
set ,
set ]
means ( $1 is
Point of
T & $1
in $2 & $2 is
open closed Subset of
T & ( $2
c= A ` or $2
c= B ` ) );
A6:
for
x being
set st
x in [#] T holds
ex
y being
set st
(
y in bool ([#] T) &
S1[
x,
y] )
proof
let x be
set ;
( x in [#] T implies ex y being set st
( y in bool ([#] T) & S1[x,y] ) )
assume A7:
x in [#] T
;
ex y being set 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 set 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
with_finite_small_inductive_dimension
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]
- 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
S1[
x,
W]
by A13, TOPGEN_1:14;
verum end;
end; consider F being
Function of
([#] T),
(bool ([#] T)) such that A16:
for
x being
set 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
by XBOOLE_0:def 10;
then A19:
RNG is
Cover of
T
by SETFAM_1:45;
RNG is
open
then consider G being
Subset-Family of
T such that A20:
G c= RNG
and A21:
G is
Cover of
T
and A22:
G is
countable
by A2, A19, METRIZTS:def 2;
not
T is
empty
by A5;
then A23:
not
G is
empty
by A21, TOPS_2:3;
then consider U being
Function of
NAT,
G such that A24:
rng U = G
by A22, CARD_3:96;
A25:
dom U = NAT
by A23, FUNCT_2:def 1;
then reconsider U =
U as
SetSequence of
([#] T) by A24, FUNCT_2:2;
consider V being
SetSequence of
([#] T) such that A26:
union (rng U) = union (rng V)
and A27:
for
i,
j being
Nat st
i <> j holds
V . i misses V . j
and A28:
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 } ;
A29:
{ (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;
A30:
rngV is
open
then
union AA is
open
by A29, TOPS_2:11, TOPS_2:19;
then reconsider UAA =
union AA,
UBB =
union (rngV \ AA) as
open Subset of
T by A30, TOPS_2:15, TOPS_2:19;
A35:
UAA misses UBB
rngV = (rngV \ AA) \/ AA
by A29, XBOOLE_1:45;
then A46:
UAA \/ UBB =
union G
by A24, A26, ZFMISC_1:78
.=
[#] T
by A21, SETFAM_1:45
;
then A47:
UAA = UBB `
by A35, PRE_TOPC:5;
B misses UAA
then A52:
B c= UAA `
by SUBSET_1:23;
A misses UBB
proof
assume
A meets UBB
;
contradiction
then consider x being
set such that A53:
x in A
and A54:
x in union (rngV \ AA)
by XBOOLE_0:3;
consider Bx being
set such that A55:
x in Bx
and A56:
Bx in rngV \ AA
by A54, TARSKI:def 4;
Bx in rngV
by A56, XBOOLE_0:def 5;
then consider m being
set such that A57:
m in dom V
and A58:
V . m = Bx
by FUNCT_1:def 3;
reconsider m =
m as
Element of
NAT by A57;
not
V . m in AA
by A56, A58, XBOOLE_0:def 5;
then
V . m meets B
;
then consider b being
set such that A59:
b in V . m
and A60:
b in B
by XBOOLE_0:3;
U . m in rng U
by A25, FUNCT_1:def 3;
then consider p being
set such that A61:
p in dom F
and A62:
F . p = U . m
by A20, A24, FUNCT_1:def 3;
reconsider Fp =
F . p as
Subset of
T by A62;
A63:
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 A28;
then
b in U . m
by A59, XBOOLE_0:def 5;
then
Fp meets B
by A60, A62, XBOOLE_0:3;
then
not
Fp c= B `
by SUBSET_1:23;
then A64:
U . m c= A `
by A16, A61, A62;
x in U . m
by A55, A58, A63, XBOOLE_0:def 5;
hence
contradiction
by A53, A64, XBOOLE_0:def 5;
verum
end; then
A c= UAA
by A47, 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 A35, A46, A47, A52;
verum end;