let S be Subset-Family of REAL; ( S = { s where s is Subset of REAL : s is left_open_interval } implies ( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover ) )
assume A1:
S = { s where s is Subset of REAL : s is left_open_interval }
; ( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover )
A2:
S is cap-closed
proof
for
S1,
S2 being
set st
S1 in S &
S2 in S holds
S1 /\ S2 in S
proof
let S1,
S2 be
set ;
( S1 in S & S2 in S implies S1 /\ S2 in S )
assume A3:
S1 in S
;
( not S2 in S or S1 /\ S2 in S )
assume A4:
S2 in S
;
S1 /\ S2 in S
consider s1 being
Subset of
REAL such that A5:
(
S1 = s1 &
s1 is
left_open_interval )
by A1, A3;
consider s2 being
Subset of
REAL such that A6:
(
S2 = s2 &
s2 is
left_open_interval )
by A1, A4;
set S3 =
s1 /\ s2;
reconsider S3 =
s1 /\ s2 as
Subset of
REAL ;
consider a1 being
R_eal,
b1 being
Real such that A7:
s1 = ].a1,b1.]
by MEASURE5:def 5, A5;
consider a2 being
R_eal,
b2 being
Real such that A8:
s2 = ].a2,b2.]
by MEASURE5:def 5, A6;
A9:
S3 = ].(max (a1,a2)),(min (b1,b2)).]
by A7, A8, XXREAL_1:141;
set m1 =
max (
a1,
a2);
max (
a1,
a2)
in ExtREAL
by XXREAL_0:def 1;
then
S3 is
left_open_interval
by A9, MEASURE5:def 5;
hence
S1 /\ S2 in S
by A1, A5, A6;
verum
end;
hence
S is
cap-closed
by FINSUB_1:def 2;
verum
end;
A10:
S is with_empty_element
then A12:
not S is empty
;
S is diff-finite-partition-closed
proof
for
S3,
S4 being
Element of
S st not
S3 \ S4 is
empty holds
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
proof
let S3,
S4 be
Element of
S;
( not S3 \ S4 is empty implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )
assume A13:
not
S3 \ S4 is
empty
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
A14:
(
S3 in S &
S4 in S )
by A12;
consider s3 being
Subset of
REAL such that A15:
(
S3 = s3 &
s3 is
left_open_interval )
by A1, A14;
consider s4 being
Subset of
REAL such that A16:
(
S4 = s4 &
s4 is
left_open_interval )
by A1, A14;
consider a1 being
R_eal,
b1 being
Real such that A17:
s3 = ].a1,b1.]
by A15, MEASURE5:def 5;
consider a2 being
R_eal,
b2 being
Real such that A18:
s4 = ].a2,b2.]
by A16, MEASURE5:def 5;
A20:
(
s4 is
empty implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
A23:
( not
s4 is
empty &
s3 misses s4 implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
( not
s4 is
empty &
s3 meets s4 implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
proof
assume A29:
( not
s4 is
empty &
s3 meets s4 )
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
then A30:
].a1,b1.] \ ].a2,b2.] = ].a1,a2.] \/ ].b2,b1.]
by A17, A18, XXREAL_1:199;
A31:
(
b1 <= b2 implies
].a1,a2.] /\ ].b2,b1.] c= {} )
A33a:
(
b2 < b1 implies
].a1,a2.] /\ ].b2,b1.] c= {} )
A40:
(
a2 in REAL or
a2 in {-infty,+infty} )
by XBOOLE_0:def 3;
A41:
(
a2 = +infty implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
by A18, A29, XXREAL_1:216;
A42:
(
a2 = -infty implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
proof
assume A43:
a2 = -infty
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
A44:
S3 \ S4 = {} \/ ].b2,b1.]
by A15, A16, A17, A18, A30, A43, XXREAL_1:212;
set z =
{].b2,b1.]};
A45:
{].b2,b1.]} c= S
{].b2,b1.]} is
a_partition of
S3 \ S4
by A44, A13, EQREL_1:39;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A45;
verum
end;
A49:
(
a2 in REAL & (
a1 < a2 or
b2 < b1 ) & ( not
a1 < a2 or not
b2 < b1 ) implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
proof
assume A50:
a2 in REAL
;
( ( not a1 < a2 & not b2 < b1 ) or ( a1 < a2 & b2 < b1 ) or ex z being finite Subset of S st z is a_partition of S3 \ S4 )
assume A51:
( (
a1 < a2 or
b2 < b1 ) & ( not
a1 < a2 or not
b2 < b1 ) )
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
A52:
(
a1 < a2 &
b1 <= b2 implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
proof
assume A53:
(
a1 < a2 &
b1 <= b2 )
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
].b2,b1.] c= {}
then A55:
].b2,b1.] = {}
;
set z =
{].a1,a2.]};
A56:
{].a1,a2.]} c= S
].a1,a2.] <> {}
then
{].a1,a2.]} is
a_partition of
].a1,a2.]
by EQREL_1:39;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A15, A16, A17, A18, A30, A55, A56;
verum
end;
(
b2 < b1 &
a2 <= a1 implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
proof
assume A58:
(
b2 < b1 &
a2 <= a1 )
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
].a1,a2.] c= {}
then A60:
].a1,a2.] = {}
;
set z =
{].b2,b1.]};
A61:
{].b2,b1.]} c= S
].b2,b1.] <> {}
by A58, XXREAL_1:2;
then
{].b2,b1.]} is
a_partition of
].b2,b1.]
by EQREL_1:39;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A15, A16, A17, A18, A30, A60, A61;
verum
end;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A51, A52;
verum
end;
A63:
(
a2 in REAL & not
a1 < a2 & not
b2 < b1 implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
(
a2 in REAL &
a1 < a2 &
b2 < b1 implies ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4 )
proof
assume A67:
a2 in REAL
;
( not a1 < a2 or not b2 < b1 or ex z being finite Subset of S st z is a_partition of S3 \ S4 )
assume
(
a1 < a2 &
b2 < b1 )
;
ex z being finite Subset of S st z is a_partition of S3 \ S4
then A69:
(
].a1,a2.] <> {} &
].b2,b1.] <> {} )
by XXREAL_1:2;
set z =
{].a1,a2.],].b2,b1.]};
A70:
{].a1,a2.],].b2,b1.]} c= S
proof
let x be
object ;
TARSKI:def 3 ( not x in {].a1,a2.],].b2,b1.]} or x in S )
assume A71:
x in {].a1,a2.],].b2,b1.]}
;
x in S
A72:
].a1,a2.] in S
].b2,b1.] in S
hence
x in S
by A71, A72, TARSKI:def 2;
verum
end;
{].a1,a2.],].b2,b1.]} is
a_partition of
].a1,b1.] \ ].a2,b2.]
proof
A73:
{].a1,a2.],].b2,b1.]} is
Subset-Family of
(].a1,b1.] \ ].a2,b2.])
proof
{].a1,a2.],].b2,b1.]} c= bool (].a1,b1.] \ ].a2,b2.])
proof
let x be
object ;
TARSKI:def 3 ( not x in {].a1,a2.],].b2,b1.]} or x in bool (].a1,b1.] \ ].a2,b2.]) )
assume
x in {].a1,a2.],].b2,b1.]}
;
x in bool (].a1,b1.] \ ].a2,b2.])
then A74:
(
x = ].a1,a2.] or
x = ].b2,b1.] )
by TARSKI:def 2;
reconsider x =
x as
set by TARSKI:1;
x c= ].a1,b1.] \ ].a2,b2.]
proof
let y be
object ;
TARSKI:def 3 ( not y in x or y in ].a1,b1.] \ ].a2,b2.] )
assume
y in x
;
y in ].a1,b1.] \ ].a2,b2.]
then
y in ].a1,a2.] \/ ].b2,b1.]
by A74, XBOOLE_0:def 3;
hence
y in ].a1,b1.] \ ].a2,b2.]
by A17, A18, A29, XXREAL_1:199;
verum
end;
hence
x in bool (].a1,b1.] \ ].a2,b2.])
;
verum
end;
hence
{].a1,a2.],].b2,b1.]} is
Subset-Family of
(].a1,b1.] \ ].a2,b2.])
;
verum
end;
A75:
union {].a1,a2.],].b2,b1.]} = ].a1,b1.] \ ].a2,b2.]
by A30, ZFMISC_1:75;
for
A being
Subset of
(].a1,b1.] \ ].a2,b2.]) st
A in {].a1,a2.],].b2,b1.]} holds
(
A <> {} & ( for
B being
Subset of
(].a1,b1.] \ ].a2,b2.]) holds
( not
B in {].a1,a2.],].b2,b1.]} or
A = B or
A misses B ) ) )
proof
let A be
Subset of
(].a1,b1.] \ ].a2,b2.]);
( A in {].a1,a2.],].b2,b1.]} implies ( A <> {} & ( for B being Subset of (].a1,b1.] \ ].a2,b2.]) holds
( not B in {].a1,a2.],].b2,b1.]} or A = B or A misses B ) ) ) )
assume A76:
A in {].a1,a2.],].b2,b1.]}
;
( A <> {} & ( for B being Subset of (].a1,b1.] \ ].a2,b2.]) holds
( not B in {].a1,a2.],].b2,b1.]} or A = B or A misses B ) ) )
for
B being
Subset of
(].a1,b1.] \ ].a2,b2.]) holds
( not
B in {].a1,a2.],].b2,b1.]} or
A = B or
A misses B )
proof
let B be
Subset of
(].a1,b1.] \ ].a2,b2.]);
( not B in {].a1,a2.],].b2,b1.]} or A = B or A misses B )
assume
B in {].a1,a2.],].b2,b1.]}
;
( A = B or A misses B )
then
( (
A = ].a1,a2.] &
B = ].a1,a2.] ) or (
A = ].a1,a2.] &
B = ].b2,b1.] ) or (
A = ].b2,b1.] &
B = ].a1,a2.] ) or (
A = ].b2,b1.] &
B = ].b2,b1.] ) )
by A76, TARSKI:def 2;
hence
(
A = B or
A misses B )
by A31, A33a;
verum
end;
hence
(
A <> {} & ( for
B being
Subset of
(].a1,b1.] \ ].a2,b2.]) holds
( not
B in {].a1,a2.],].b2,b1.]} or
A = B or
A misses B ) ) )
by A69, A76;
verum
end;
hence
{].a1,a2.],].b2,b1.]} is
a_partition of
].a1,b1.] \ ].a2,b2.]
by A73, A75, EQREL_1:def 4;
verum
end;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A15, A16, A17, A18, A70;
verum
end;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A40, A41, A42, A49, A63, TARSKI:def 2;
verum
end;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A20, A23;
verum
end;
hence
S is
diff-finite-partition-closed
by SRINGS_1:def 2;
verum
end;
hence
( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover )
by A1, A2, A10, LemmB; verum