:: On the {K}uratowski Closure-Complement Problem
:: by Lilla Krystyna Bagi\'nska and Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PRE_TOPC, SUBSET_1, ARYTM_1, TOPS_1, TARSKI,
STRUCT_0, SETFAM_1, FINSET_1, ZFMISC_1, CARD_1, XXREAL_0, ARYTM_3,
TOPMETR, XXREAL_1, BORSUK_5, RCOMP_1, PROB_1, KURATO_1;
notations XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, CARD_1,
ORDINAL1, NUMBERS, XXREAL_0, PRE_TOPC, TOPS_1, ENUMSET1, FINSET_1,
RCOMP_1, NAT_1, SEQ_4, TOPMETR, TOPS_2, BORSUK_5, PROB_1;
constructors PROB_1, RCOMP_1, TOPS_1, TOPS_2, TOPMETR, BORSUK_5, SEQ_4,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, XXREAL_0, MEMBERED,
TOPS_1, TOPMETR, BORSUK_5, STRUCT_0;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
definitions TARSKI, SETFAM_1;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, ZFMISC_1, TOPS_2;
theorems ENUMSET1, TOPS_1, PRE_TOPC, CARD_2, XBOOLE_0, TDLAT_1, TARSKI,
TOPMETR, ZFMISC_1, XBOOLE_1, SETFAM_1, MEASURE1, BORSUK_5, TOPS_2,
PROB_1, XREAL_1, XXREAL_0, XXREAL_1, XREAL_0;
begin :: Fourteen Kuratowski Sets
reserve T for non empty TopSpace;
reserve A for Subset of T;
notation
let T be non empty TopSpace, A be Subset of T;
synonym A- for Cl A;
end;
theorem Th1:
A-`-`-`- = A-`-
proof
set B = Cl (Cl A)`;
set U = (Cl A)`;
U = Int U by TOPS_1:23;
then U c= Int Cl U by PRE_TOPC:18,TOPS_1:19;
then Cl Int B c= Cl B & Cl U c= Cl Int Cl U by PRE_TOPC:19,TOPS_1:16;
then Cl Int B = B by XBOOLE_0:def 10;
hence thesis by TOPS_1:def 1;
end;
Lm1: for T being 1-sorted, A, B being Subset-Family of T holds A \/ B is
Subset-Family of T;
definition
let T, A;
func Kurat14Part A -> set equals
{ A, A-, A-`, A-`-, A-`-`, A-`-`-, A-`-`-` };
coherence;
end;
registration
let T, A;
cluster Kurat14Part A -> finite;
coherence;
end;
definition
let T, A;
func Kurat14Set A -> Subset-Family of T equals
{ A, A-, A-`, A-`-, A-`-`, A-
`-`-, A-`-`-` } \/ { A`, A`-, A`-`, A`-`-, A`-`-`, A`-`-`-, A`-`-`-` };
coherence
proof
set X1 = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl A)`)`,
(Cl (Cl (Cl A)`)`)` }, X2 = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
X2 c= bool the carrier of T
proof
let x be object;
assume x in X2;
then
x = A` or x = Cl A` or x = (Cl A`)` or x = Cl (Cl A`)` or x = (Cl (
Cl A`)`)` or x = Cl (Cl (Cl A`)`)` or x = (Cl (Cl (Cl A`)`)`)` by
ENUMSET1:def 5;
hence thesis;
end;
then reconsider X2 as Subset-Family of T;
X1 c= bool the carrier of T
proof
let x be object;
assume x in X1;
then
x = A or x = Cl A or x = (Cl A)` or x = Cl (Cl A)` or x = (Cl (Cl A)
`)` or x = Cl (Cl (Cl A)`)` or x = (Cl (Cl (Cl A)`)`)` by ENUMSET1:def 5;
hence thesis;
end;
then reconsider X1 as Subset-Family of T;
X1 \/ X2 is Subset-Family of T;
hence thesis;
end;
end;
theorem
Kurat14Set A = Kurat14Part A \/ Kurat14Part A`;
theorem Th3:
A in Kurat14Set A & A- in Kurat14Set A & A-` in Kurat14Set A & A-
`- in Kurat14Set A & A-`-` in Kurat14Set A & A-`-`- in Kurat14Set A & A-`-`-`
in Kurat14Set A
proof
A1: Cl A in Kurat14Part A & (Cl A)` in Kurat14Part A by ENUMSET1:def 5;
A2: Cl (Cl A)` in Kurat14Part A & (Cl (Cl A)`)` in Kurat14Part A by
ENUMSET1:def 5;
A3: Cl (Cl (Cl A)`)` in Kurat14Part A & (Cl (Cl (Cl A)`)`)` in Kurat14Part A
by ENUMSET1:def 5;
Kurat14Part A c= Kurat14Set A & A in Kurat14Part A by ENUMSET1:def 5
,XBOOLE_1:7;
hence thesis by A1,A2,A3;
end;
theorem Th4:
A` in Kurat14Set A & A`- in Kurat14Set A & A`-` in Kurat14Set A &
A`-`- in Kurat14Set A & A`-`-` in Kurat14Set A & A`-`-`- in Kurat14Set A & A`-`
-`-` in Kurat14Set A
proof
A1: Cl A` in Kurat14Part A` & (Cl A`)` in Kurat14Part A` by ENUMSET1:def 5;
A2: Cl (Cl A`)` in Kurat14Part A` & (Cl (Cl A`)`)` in Kurat14Part A` by
ENUMSET1:def 5;
A3: Cl (Cl (Cl A`)`)` in Kurat14Part A` & (Cl (Cl (Cl A`)`)`)` in
Kurat14Part A` by ENUMSET1:def 5;
Kurat14Part A` c= Kurat14Set A & A` in Kurat14Part A` by ENUMSET1:def 5
,XBOOLE_1:7;
hence thesis by A1,A2,A3;
end;
definition
let T, A;
func Kurat14ClPart A -> Subset-Family of T equals
{ A-, A-`-, A-`-`-, A`-, A
`-`-, A`-`-`- };
coherence
proof
A1: { Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } is Subset-Family of T by
MEASURE1:3;
{Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`
)`)`} = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } \/ { Cl A`, Cl (Cl A`)`, Cl (Cl
(Cl A`)` )` } & { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } is Subset-Family of T
by ENUMSET1:13,MEASURE1:3;
hence thesis by A1,Lm1;
end;
func Kurat14OpPart A -> Subset-Family of T equals
{ A-`, A-`-`, A-`-`-`, A`-
`, A`-`-`, A`-`-`-` };
coherence
proof
A2: { (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } is Subset-Family of
T by MEASURE1:3;
{ (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`, (Cl A`)`, (Cl (Cl A`)`)
`, (Cl (Cl (Cl A`)`)`)` } = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
{ (Cl A `)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } & { (Cl A)`, (Cl (Cl A)`)`,
(Cl ( Cl (Cl A)`)`)` } is Subset-Family of T by ENUMSET1:13,MEASURE1:3;
hence thesis by A2,Lm1;
end;
end;
Lm2: Kurat14Set A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`,
Cl (Cl (Cl A`)`)` } \/ { A, A` } \/ { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`
)`, (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` }
proof
set Y1 = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (
Cl A`)`)` }, Y2 = { A, A` }, Y3 = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`
, (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
set Y = Y1 \/ Y2 \/ Y3;
A1: Y3 c= Y by XBOOLE_1:7;
A2: Y c= Kurat14Set A
proof
let x be object;
assume x in Y;
then
A3: x in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl
(Cl A`)`)` } \/ { A, A` } or x in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`
, (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 3;
per cases by A3,XBOOLE_0:def 3;
suppose
x in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`,
Cl (Cl (Cl A`)`)` };
then x = Cl A or x = Cl (Cl A)` or x = Cl (Cl (Cl A)`)` or x = Cl A` or
x = Cl (Cl A`)` or x = Cl (Cl (Cl A`)`)` by ENUMSET1:def 4;
hence thesis by Th3,Th4;
end;
suppose
x in { A, A` };
then x = A or x = A` by TARSKI:def 2;
hence thesis by Th3,Th4;
end;
suppose
x in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`, (Cl A`)`, (
Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
then x = (Cl A)` or x = (Cl (Cl A)`)` or x = (Cl (Cl (Cl A)`)`)` or x =
(Cl A`)` or x = (Cl (Cl A`)`)` or x = (Cl (Cl (Cl A`)`)`)` by ENUMSET1:def 4;
hence thesis by Th3,Th4;
end;
end;
A4: Y1 \/ Y2 c= Y by XBOOLE_1:7;
(Cl (Cl A)`)` in Y3 by ENUMSET1:def 4;
then
A5: (Cl (Cl A)`)` in Y by A1;
(Cl A)` in Y3 by ENUMSET1:def 4;
then
A6: (Cl A)` in Y by A1;
Y2 c= Y1 \/ Y2 by XBOOLE_1:7;
then
A7: Y2 c= Y by A4;
(Cl (Cl (Cl A`)`)`)` in Y3 by ENUMSET1:def 4;
then
A8: (Cl (Cl (Cl A`)`)`)` in Y by A1;
(Cl (Cl A`)`)` in Y3 by ENUMSET1:def 4;
then
A9: (Cl (Cl A`)`)` in Y by A1;
(Cl A`)` in Y3 by ENUMSET1:def 4;
then
A10: (Cl A`)` in Y by A1;
(Cl (Cl (Cl A)`)`)` in Y3 by ENUMSET1:def 4;
then
A11: (Cl (Cl (Cl A)`)`)` in Y by A1;
A in Y2 by TARSKI:def 2;
then
A12: A in Y by A7;
Y1 c= Y1 \/ Y2 by XBOOLE_1:7;
then
A13: Y1 c= Y by A4;
A` in Y2 by TARSKI:def 2;
then
A14: A` in Y by A7;
Cl (Cl (Cl A`)`)` in Y1 by ENUMSET1:def 4;
then
A15: Cl (Cl (Cl A`)`)` in Y by A13;
Cl (Cl A`)` in Y1 by ENUMSET1:def 4;
then
A16: Cl (Cl A`)` in Y by A13;
Cl A` in Y1 by ENUMSET1:def 4;
then
A17: Cl A` in Y by A13;
Cl (Cl (Cl A)`)` in Y1 by ENUMSET1:def 4;
then
A18: Cl (Cl (Cl A)`)` in Y by A13;
Cl (Cl A)` in Y1 by ENUMSET1:def 4;
then
A19: Cl (Cl A)` in Y by A13;
Cl A in Y1 by ENUMSET1:def 4;
then
A20: Cl A in Y by A13;
Kurat14Set A c= Y
proof
let x be object;
assume
A21: x in Kurat14Set A;
per cases by A21,XBOOLE_0:def 3;
suppose
x in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` };
hence thesis by A20,A19,A18,A12,A6,A5,A11,ENUMSET1:def 5;
end;
suppose
x in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`, Cl (Cl
(Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
hence thesis by A17,A16,A15,A14,A10,A9,A8,ENUMSET1:def 5;
end;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem
Kurat14Set A = { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A by Lm2;
registration
let T, A;
cluster Kurat14Set A -> finite;
coherence;
end;
theorem Th6:
for Q being Subset of T holds Q in Kurat14Set A implies Q` in
Kurat14Set A & Q- in Kurat14Set A
proof
let Q be Subset of T;
set k1 = Cl A, k2 = (Cl A)`, k3 = Cl (Cl A)`, k4 = (Cl (Cl A)`)`, k5 = Cl (
Cl (Cl A)`)`, k6 = (Cl (Cl (Cl A)`)`)`, k7 = Cl A`, k8 = (Cl A`)`, k9 = Cl (Cl
A`)`, k10 = (Cl (Cl A`)`)`, k11 = Cl (Cl (Cl A`)`)`, k12 = (Cl (Cl (Cl A`)`)`)`
;
assume
A1: Q in Kurat14Set A;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: Q in { A, k1, k2, k3, k4, k5, k6 };
Q` in Kurat14Set A & Cl Q in Kurat14Set A
proof
per cases by A2,ENUMSET1:def 5;
suppose
Q = A;
then
Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (
Cl A`)`)`, Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = Cl A;
then
Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, k3, k4, k5, k6 } by
ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = (Cl A)`;
then
Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, Cl A, (Cl A)`, k3, k4, k5, k6 } by
ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = Cl (Cl A)`;
then
Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, k3, k4, k5, k6 } by
ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = (Cl (Cl A)`)`;
then
Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, Cl (Cl A)`, k4, k5, k6 } by
ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = Cl (Cl (Cl A)`)`;
then
Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } & Q` in { A, k1, k2, k3, k4, k5, k6 } by
ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A3: Q = (Cl (Cl (Cl A)`)`)`;
Cl (Cl (Cl (Cl A)`)`)` = Cl (Cl A)` by Th1;
then
A4: Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl
A)`)`, (Cl (Cl (Cl A)`)`)` } by A3,ENUMSET1:def 5;
Q` in { A, k1, k2, k3, k4, k5, k6 } by A3,ENUMSET1:def 5;
hence thesis by A4,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
suppose
A5: Q in { A`, k7, k8, k9, k10, k11, k12 };
Q` in Kurat14Set A & Cl Q in Kurat14Set A
proof
per cases by A5,ENUMSET1:def 5;
suppose
Q = A`;
then
Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12 } & Q` in { A, k1, k2,
k3, k4, k5, k6 } by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = Cl A`;
then
Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12} & Q` in { A`, k7, (Cl
A`)`, k9, k10, k11, k12} by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = (Cl A`)`;
then Cl Q in { A`, k7, k8, Cl (Cl A`)`, k10, k11, k12} & Q` in { A`,
Cl A`, k8, k9, k10, k11, k12} by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = Cl (Cl A`)`;
then
Cl Q in { A`, k7, k8, k9, k10, k11, k12} & Q` in { A`, k7, k8, k9
, k10, k11, k12} by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = (Cl (Cl A`)`)`;
then
Cl Q in { A`, k7, k8, k9, k10, k11, k12} & Q` in { A`, k7, k8, k9
, k10, k11, k12} by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q = Cl (Cl (Cl A`)`)`;
then
Cl Q in { A`, k7, k8, k9, k10, k11, k12} & Q` in { A`, k7, k8, k9
, k10, k11, k12} by ENUMSET1:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A6: Q = (Cl (Cl (Cl A`)`)`)`;
then Cl Q = Cl (Cl A`)` by Th1;
then
A7: Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:def 5;
Q` in { A`, k7, k8, k9, k10, k11, k12} by A6,ENUMSET1:def 5;
hence thesis by A7,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
end;
theorem
card Kurat14Set A <= 14
proof
set X = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`, Cl (Cl (Cl A)`)`, (Cl
(Cl (Cl A)`)`)` }, Y = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`, Cl (
Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
card X <= 7 & card Y <= 7 by CARD_2:55;
then card (X \/ Y) <= card X + card Y & card X + card Y <= 7 + 7 by CARD_2:43
,XREAL_1:7;
hence thesis by XXREAL_0:2;
end;
begin :: Seven Kuratowski Sets
definition
let T, A;
func Kurat7Set A -> Subset-Family of T equals
{ A, Int A, Cl A, Int Cl A, Cl
Int A, Cl Int Cl A, Int Cl Int A };
coherence
proof
set X = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A };
X c= bool the carrier of T
proof
let x be object;
assume x in X;
then
x = A or x = Int A or x = Cl A or x = Int Cl A or x = Cl Int A or x
= Cl Int Cl A or x = Int Cl Int A by ENUMSET1:def 5;
hence thesis;
end;
hence thesis;
end;
end;
theorem
Kurat7Set A = { A } \/ { Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl
Int A, Cl Int Cl A }
proof
Kurat7Set A = { A } \/ { Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
Int Cl Int A } by ENUMSET1:16
.= { A } \/ ({ Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl Int A, Cl
Int Cl A }) by BORSUK_5:2
.= { A } \/ { Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl Int A, Cl
Int Cl A } by XBOOLE_1:4;
hence thesis;
end;
registration
let T, A;
cluster Kurat7Set A -> finite;
coherence;
end;
theorem Th9:
for Q being Subset of T holds Q in Kurat7Set A implies Int Q in
Kurat7Set A & Cl Q in Kurat7Set A
proof
let Q be Subset of T;
assume
A1: Q in Kurat7Set A;
Int Q in Kurat7Set A & Cl Q in Kurat7Set A
proof
per cases by A1,ENUMSET1:def 5;
suppose
Q = A;
hence thesis by ENUMSET1:def 5;
end;
suppose
Q = Int A;
hence thesis by ENUMSET1:def 5;
end;
suppose
Q = Cl A;
hence thesis by ENUMSET1:def 5;
end;
suppose
Q = Int Cl A;
hence thesis by ENUMSET1:def 5;
end;
suppose
Q = Cl Int A;
hence thesis by ENUMSET1:def 5;
end;
suppose
A2: Q = Cl Int Cl A;
Int Cl Int Cl A = Int Cl A by TDLAT_1:5;
hence thesis by A2,ENUMSET1:def 5;
end;
suppose
A3: Q = Int Cl Int A;
then Cl Q = Cl Int A by TOPS_1:26;
hence thesis by A3,ENUMSET1:def 5;
end;
end;
hence thesis;
end;
begin :: The Set Generating Exactly Fourteen Kuratowski Sets
definition
func KurExSet -> Subset of R^1 equals
{1} \/ RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5
,+infty .[;
coherence by TOPMETR:17;
end;
theorem Th10:
Cl KurExSet = {1} \/ [. 2,+infty .[
proof
set A = KurExSet;
reconsider B = {1}, C = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[ as Subset
of R^1 by TOPMETR:17;
A = {1} \/ (RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[) by XBOOLE_1:113;
then
A1: Cl A = Cl B \/ Cl C by PRE_TOPC:20;
Cl B = {1} by BORSUK_5:38;
hence thesis by A1,BORSUK_5:56;
end;
theorem Th11:
(Cl KurExSet)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ by Th10,BORSUK_5:63;
theorem Th12:
Cl (Cl KurExSet)` = ]. -infty, 2 .] by Th11,BORSUK_5:64;
theorem Th13:
(Cl (Cl KurExSet)`)` = ]. 2,+infty .[ by Th12,TOPMETR:17,XXREAL_1:224,288;
theorem Th14:
Cl (Cl (Cl KurExSet)`)` = [. 2,+infty .[ by Th13,BORSUK_5:49;
theorem Th15:
(Cl (Cl (Cl KurExSet)`)`)` = ]. -infty, 2 .[ by Th14,TOPMETR:17,XXREAL_1:224
,294;
theorem Th16:
KurExSet` = ]. -infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
set A = KurExSet;
reconsider B = {1}, C = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[ as Subset
of R^1 by TOPMETR:17;
A1: C` = ]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5} by BORSUK_5:60;
A = {1} \/ (RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[) & B` = ]. -infty,
1 .[ \/ ]. 1,+infty .[ by BORSUK_5:61,XBOOLE_1:113;
hence thesis by A1,BORSUK_5:62,XBOOLE_1:53;
end;
theorem Th17:
Cl KurExSet` = ]. -infty, 4 .] \/ {5} by Th16,BORSUK_5:67;
theorem Th18:
(Cl KurExSet`)` = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th17,BORSUK_5:68;
theorem Th19:
Cl (Cl KurExSet`)` = [. 4,+infty .[ by Th18,BORSUK_5:55;
theorem Th20:
(Cl (Cl KurExSet`)`)` = ]. -infty, 4 .[ by Th19,TOPMETR:17,XXREAL_1:224,294;
theorem Th21:
Cl (Cl (Cl KurExSet`)`)` = ]. -infty, 4 .] by Th20,BORSUK_5:51;
theorem Th22:
(Cl (Cl (Cl KurExSet`)`)`)` = ]. 4,+infty .[ by Th21,TOPMETR:17,XXREAL_1:224
,288;
begin :: The Set Generating Exactly Seven Kuratowski Sets
theorem Th23:
Int KurExSet = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,TOPS_1:def 1;
theorem Th24:
Cl Int KurExSet = [. 4,+infty .[ by Th18,BORSUK_5:55,TOPS_1:def 1;
theorem Th25:
Int Cl Int KurExSet = ]. 4,+infty .[
proof
set A = KurExSet;
Cl Int A = Cl (Cl A`)` by TOPS_1:def 1;
then
A1: Int Cl Int A = (Cl (Cl (Cl A`)`)`)` by TOPS_1:def 1;
(Cl (Cl A`)`)` = ]. -infty, 4 .[ by Th19,TOPMETR:17,XXREAL_1:224,294;
then Cl (Cl (Cl A`)`)` = ]. -infty, 4 .] by BORSUK_5:51;
hence thesis by A1,TOPMETR:17,XXREAL_1:224,288;
end;
theorem Th26:
Int Cl KurExSet = ]. 2,+infty .[
proof
set A = KurExSet;
(Cl A)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ by Th10,BORSUK_5:63;
then Cl (Cl A)` = ]. -infty, 2 .] by BORSUK_5:64;
then (Cl (Cl A)`)` = ]. 2,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
hence thesis by TOPS_1:def 1;
end;
theorem Th27:
Cl Int Cl KurExSet = [. 2,+infty .[
proof
set A = KurExSet;
(Cl A)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ by Th10,BORSUK_5:63;
then Cl (Cl A)` = ]. -infty, 2 .] by BORSUK_5:64;
then (Cl (Cl A)`)` = ]. 2,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
hence thesis by BORSUK_5:49,TOPS_1:def 1;
end;
begin :: The Difference Between Chosen Kuratowski Sets
theorem
Cl Int Cl KurExSet <> Int Cl KurExSet
by Th27,XXREAL_1:236,Th26,XXREAL_1:235;
theorem Th29:
Cl Int Cl KurExSet <> Cl KurExSet
proof
set A = KurExSet;
1 in {1} by TARSKI:def 1;
then 1 in Cl A by Th10,XBOOLE_0:def 3;
hence thesis by Th27,XXREAL_1:236;
end;
theorem
Cl Int Cl KurExSet <> Int Cl Int KurExSet
by Th27,XXREAL_1:236,Th25,XXREAL_1:235;
theorem Th31:
Cl Int Cl KurExSet <> Cl Int KurExSet
proof
set A = KurExSet;
2 in Cl Int Cl A by Th27,XXREAL_1:236;
hence thesis by Th24,XXREAL_1:236;
end;
theorem
Cl Int Cl KurExSet <> Int KurExSet
proof
set A = KurExSet;
2 in Cl Int Cl A & Int A = ]. 4, 5.[ \/ ]. 5,+infty .[ by Th18,Th27,
TOPS_1:def 1,XXREAL_1:236;
hence thesis by XXREAL_1:223;
end;
theorem
Int Cl KurExSet <> Cl KurExSet
proof
set A = KurExSet;
1 in {1} by TARSKI:def 1;
then 1 in Cl A by Th10,XBOOLE_0:def 3;
hence thesis by Th26,XXREAL_1:235;
end;
theorem
Int Cl KurExSet <> Int Cl Int KurExSet
proof
set A = KurExSet;
3 in Int Cl A by Th26,XXREAL_1:235;
hence thesis by Th25,XXREAL_1:235;
end;
theorem
Int Cl KurExSet <> Cl Int KurExSet by Th26,BORSUK_5:34,45;
theorem Th36:
Int Cl KurExSet <> Int KurExSet
proof
set A = KurExSet;
5 in Int Cl A & Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,Th26,
TOPS_1:def 1,XXREAL_1:235;
hence thesis by XXREAL_1:205;
end;
theorem
Int Cl Int KurExSet <> Cl KurExSet
proof
set A = KurExSet;
2 in [. 2,+infty .[ by XXREAL_1:236;
then 2 in Cl A by Th10,XBOOLE_0:def 3;
hence thesis by Th25,XXREAL_1:235;
end;
theorem Th38:
Cl Int KurExSet <> Cl KurExSet
proof
set A = KurExSet;
2 in [. 2,+infty .[ by XXREAL_1:236;
then 2 in Cl A by Th10,XBOOLE_0:def 3;
hence thesis by Th24,XXREAL_1:236;
end;
theorem
Int KurExSet <> Cl KurExSet
proof
set A = KurExSet;
5 in [. 2,+infty .[ by XXREAL_1:236;
then
A1: 5 in Cl A by Th10,XBOOLE_0:def 3;
Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,TOPS_1:def 1;
hence thesis by A1,XXREAL_1:205;
end;
theorem Th40:
Cl KurExSet <> KurExSet
proof
set A = KurExSet;
( not 5 in {1})& not 5 in RAT (2, 4) by BORSUK_5:29,TARSKI:def 1;
then ( not 5 in ]. 4, 5 .[)& not 5 in {1} \/ RAT (2, 4) by XBOOLE_0:def 3
,XXREAL_1:4;
then
A1: ( not 5 in ]. 5,+infty .[)& not 5 in {1} \/ RAT (2, 4) \/ ]. 4, 5 .[ by
XBOOLE_0:def 3,XXREAL_1:235;
5 in [. 2,+infty .[ by XXREAL_1:236;
then 5 in Cl A by Th10,XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th41:
KurExSet <> Int KurExSet
proof
set A = KurExSet;
1 in { 1 } by TARSKI:def 1;
then 1 in {1} \/ RAT (2,4) by XBOOLE_0:def 3;
then 1 in {1} \/ RAT (2,4) \/ ]. 4, 5 .[ by XBOOLE_0:def 3;
then
A1: 1 in A by XBOOLE_0:def 3;
Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,TOPS_1:def 1;
hence thesis by A1,XXREAL_1:223;
end;
theorem
Cl Int KurExSet <> Int Cl Int KurExSet
by Th24,XXREAL_1:236,Th25,XXREAL_1:235;
theorem Th43:
Int Cl Int KurExSet <> Int KurExSet
proof
set A = KurExSet;
5 in Int Cl Int A & Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,Th25,
TOPS_1:def 1,XXREAL_1:235;
hence thesis by XXREAL_1:205;
end;
theorem
Cl Int KurExSet <> Int KurExSet
proof
set A = KurExSet;
4 in Cl Int A & Int A = ]. 4, 5 .[ \/ ]. 5,+infty .[ by Th18,Th24,
TOPS_1:def 1,XXREAL_1:236;
hence thesis by XXREAL_1:223;
end;
begin :: Final Proofs For Seven
theorem Th45:
Int Cl Int KurExSet <> Int Cl KurExSet
proof
set A = KurExSet;
not 3 in Int Cl Int A by Th25,XXREAL_1:235;
hence thesis by Th26,XXREAL_1:235;
end;
theorem Th46:
Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet are_mutually_distinct
by Th36,Th43,Th45;
theorem Th47:
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct
by Th38,Th29,Th31;
theorem Th48:
for X being set st X in { Int KurExSet, Int Cl KurExSet, Int Cl
Int KurExSet } holds X is open non empty Subset of R^1
proof
let X be set;
assume
A1: X in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet };
per cases by A1,ENUMSET1:def 1;
suppose
X = Int KurExSet;
hence thesis by Th18,TOPS_1:def 1;
end;
suppose
X = Int Cl KurExSet;
hence thesis by Th26;
end;
suppose
X = Int Cl Int KurExSet;
hence thesis by Th25;
end;
end;
theorem Th49:
for X being set st X in { Int KurExSet, Int Cl KurExSet, Int Cl
Int KurExSet } holds X <> REAL
proof
let X be set;
assume
A1: X in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet };
per cases by A1,ENUMSET1:def 1;
suppose
A2: X = Int KurExSet;
5 in REAL by XREAL_0:def 1;
hence thesis by Th23,XXREAL_1:205,A2;
end;
suppose
X = Int Cl KurExSet;
hence thesis by Th26,BORSUK_5:45;
end;
suppose
X = Int Cl Int KurExSet;
hence thesis by Th25,BORSUK_5:45;
end;
end;
theorem
for X being set st X in { Cl KurExSet, Cl Int KurExSet, Cl Int Cl
KurExSet } holds X <> REAL
proof
let X be set;
assume
A1: X in { Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };
per cases by A1,ENUMSET1:def 1;
suppose
A2: X = Cl KurExSet;
A3: 0 in REAL by XREAL_0:def 1;
( not 0 in {1})& not 0 in [. 2,+infty .[ by XXREAL_1:236, TARSKI:def 1;
hence thesis by A2,Th10,XBOOLE_0:def 3,A3;
end;
suppose
X = Cl Int KurExSet;
hence thesis by Th24,BORSUK_5:46;
end;
suppose
X = Cl Int Cl KurExSet;
hence thesis by Th27,BORSUK_5:46;
end;
end;
theorem Th51:
{ Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet } misses {
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet }
proof
set X = { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet }, Y = { Cl
KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };
assume X meets Y;
then consider x being object such that
A1: x in X and
A2: x in Y by XBOOLE_0:3;
x is open non empty Subset of R^1 & x is closed Subset of R^1 by A1,A2,Th48,
ENUMSET1:def 1;
hence thesis by A1,Th49,BORSUK_5:34;
end;
theorem Th52:
Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl KurExSet,
Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct by Th46,Th47,Th51,
BORSUK_5:6;
registration
cluster KurExSet -> non closed non open;
coherence by Th40,Th41,PRE_TOPC:22,TOPS_1:23;
end;
theorem
{ Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl
KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } misses { KurExSet }
proof
set A = KurExSet;
assume { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl KurExSet,
Cl Int KurExSet, Cl Int Cl KurExSet } meets { KurExSet };
then
A1: KurExSet in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl
KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } by ZFMISC_1:50;
per cases by A1,ENUMSET1:def 4;
suppose
A = Int A;
hence thesis;
end;
suppose
A = Int Cl A;
hence thesis;
end;
suppose
A = Int Cl Int A;
hence thesis;
end;
suppose
A = Cl A;
hence thesis;
end;
suppose
A = Cl Int A;
hence thesis;
end;
suppose
A = Cl Int Cl A;
hence thesis;
end;
end;
theorem Th54:
KurExSet, Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl
KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct
by Th52;
theorem
card Kurat7Set KurExSet = 7
proof
set A = KurExSet;
A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A
are_mutually_distinct by Th54;
hence thesis by BORSUK_5:4;
end;
begin :: Final Proofs For Fourteen
registration
cluster Kurat14ClPart KurExSet -> with_proper_subsets;
coherence
proof
set A = KurExSet;
assume
A1: the carrier of R^1 in Kurat14ClPart KurExSet;
per cases by A1,ENUMSET1:def 4,TOPMETR:17;
suppose
REAL = Cl A;
hence thesis by Th10,BORSUK_5:69;
end;
suppose
REAL = Cl (Cl A)`;
hence thesis by Th12,BORSUK_5:47;
end;
suppose
REAL = Cl (Cl (Cl A)`)`;
hence thesis by Th14,BORSUK_5:46;
end;
suppose
REAL = Cl A`;
hence thesis by Th17,BORSUK_5:70;
end;
suppose
REAL = Cl (Cl A`)`;
hence thesis by Th19,BORSUK_5:46;
end;
suppose
REAL = Cl (Cl (Cl A`)`)`;
hence thesis by Th21,BORSUK_5:47;
end;
end;
cluster Kurat14OpPart KurExSet -> with_proper_subsets;
coherence
proof
set A = KurExSet;
assume
A2: the carrier of R^1 in Kurat14OpPart KurExSet;
per cases by A2,ENUMSET1:def 4,TOPMETR:17;
suppose
REAL = (Cl A)`;
hence thesis by Th10,BORSUK_5:72;
end;
suppose
REAL = (Cl (Cl A)`)`;
hence thesis by Th12,BORSUK_5:72;
end;
suppose
REAL = (Cl (Cl (Cl A)`)`)`;
hence thesis by Th14,BORSUK_5:72;
end;
suppose
REAL = (Cl A`)`;
hence thesis by Th17,BORSUK_5:72;
end;
suppose
REAL = (Cl (Cl A`)`)`;
hence thesis by Th19,BORSUK_5:72;
end;
suppose
REAL = (Cl (Cl (Cl A`)`)`)`;
hence thesis by Th21,BORSUK_5:72;
end;
end;
end;
registration
cluster Kurat14Set KurExSet -> with_proper_subsets;
coherence
proof
reconsider AA = { KurExSet, KurExSet` } as Subset-Family of R^1 by
MEASURE1:2;
AA is with_proper_subsets
proof
assume
A1: the carrier of R^1 in AA;
per cases by A1,TARSKI:def 2,TOPMETR:17;
suppose
REAL = KurExSet;
then [#]R^1 = KurExSet by TOPMETR:17;
hence thesis;
end;
suppose
REAL = KurExSet`;
then [#]R^1 = KurExSet` by TOPMETR:17;
hence thesis by TOPS_1:3;
end;
end;
then
A2: AA \/ Kurat14ClPart KurExSet is with_proper_subsets by SETFAM_1:48;
Kurat14Set KurExSet = AA \/ Kurat14ClPart KurExSet \/ Kurat14OpPart
KurExSet by Lm2;
hence thesis by A2,SETFAM_1:48;
end;
end;
registration
cluster Kurat14Set KurExSet -> with_non-empty_elements;
coherence
proof
reconsider E = {}R^1 as Subset of R^1;
assume {} in Kurat14Set KurExSet;
then E` in Kurat14Set KurExSet by Th6;
hence thesis by SETFAM_1:def 12;
end;
end;
theorem Th56:
for A being with_non-empty_elements set, B being set st B c= A
holds B is with_non-empty_elements
proof
let A be with_non-empty_elements set, B be set;
assume
A1: B c= A;
assume {} in B;
hence thesis by A1;
end;
registration
cluster Kurat14ClPart KurExSet -> with_non-empty_elements;
coherence
proof
Kurat14Set KurExSet = { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet
\/ Kurat14OpPart KurExSet by Lm2;
then
A1: { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet c= Kurat14Set
KurExSet by XBOOLE_1:7;
Kurat14ClPart KurExSet c= { KurExSet, KurExSet`} \/ Kurat14ClPart
KurExSet by XBOOLE_1:7;
hence thesis by A1,Th56,XBOOLE_1:1;
end;
cluster Kurat14OpPart KurExSet -> with_non-empty_elements;
coherence
proof
Kurat14Set KurExSet = { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet
\/ Kurat14OpPart KurExSet by Lm2;
hence thesis by Th56,XBOOLE_1:7;
end;
end;
registration
cluster with_proper_subsets with_non-empty_elements for Subset-Family of R^1;
existence
proof
take Kurat14Set KurExSet;
thus thesis;
end;
end;
theorem Th57:
for F, G being with_proper_subsets with_non-empty_elements
Subset-Family of R^1 st F is open & G is closed holds F misses G
proof
let F, G be with_proper_subsets with_non-empty_elements Subset-Family of R^1;
assume
A1: F is open & G is closed;
assume F meets G;
then consider x being object such that
A2: x in F and
A3: x in G by XBOOLE_0:3;
reconsider x as Subset of R^1 by A2;
x is open & x is closed by A1,A2,A3;
then x = {} or x = REAL by BORSUK_5:34;
hence thesis by A2,SETFAM_1:def 12,TOPMETR:17;
end;
registration
cluster Kurat14ClPart KurExSet -> closed;
coherence
by ENUMSET1:def 4;
cluster Kurat14OpPart KurExSet -> open;
coherence
by ENUMSET1:def 4;
end;
theorem
Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th57;
registration
let T, A;
cluster Kurat14ClPart A -> finite;
coherence;
cluster Kurat14OpPart A -> finite;
coherence;
end;
theorem Th59:
card (Kurat14ClPart KurExSet) = 6
proof
set A = KurExSet;
A1: Cl (Cl (Cl A`)`)` = ]. -infty, 4 .] by Th20,BORSUK_5:51;
5 in {5} by TARSKI:def 1;
then 5 in Cl A` by Th17,XBOOLE_0:def 3;
then
A2: Cl Int A = Cl (Cl A`)` & Cl A` <> Cl (Cl (Cl A`)`)` by A1,TOPS_1:def 1
,XXREAL_1:234;
( not 5 in Cl (Cl (Cl A`)`)`)& 5 in [. 2,+infty .[ by Th21,XXREAL_1:234,236;
then
A3: Cl A <> Cl (Cl (Cl A`)`)` by Th10,XBOOLE_0:def 3;
( not 5 in Cl (Cl (Cl A`)`)`)& Cl (Cl A`)` = [. 4,+infty .[ by Th18,Th21,
BORSUK_5:55,XXREAL_1:234;
then
A4: Cl (Cl A`)` <> Cl (Cl (Cl A`)`)` by XXREAL_1:236;
5 in Cl (Cl (Cl A)`)` by Th14,XXREAL_1:236;
then
A5: Cl (Cl (Cl A)`)` <> Cl (Cl (Cl A`)`)` by Th21,XXREAL_1:234;
( not 6 in ]. -infty, 4 .])& not 6 in {5} by TARSKI:def 1,XXREAL_1:234;
then
A6: not 6 in Cl A` by Th17,XBOOLE_0:def 3;
Cl (Cl (Cl A)`)` = [. 2,+infty .[ by Th13,BORSUK_5:49;
then
A7: Cl (Cl (Cl A)`)` <> Cl A` by A6,XXREAL_1:236;
A8: 4 in Cl (Cl (Cl A)`)` & Cl Int Cl A = Cl (Cl (Cl A)`)` by Th14,TOPS_1:def 1
,XXREAL_1:236;
A9: not 4 in Cl (Cl A)` by Th12,XXREAL_1:234;
then Cl (Cl A)` <> Cl (Cl (Cl A`)`)` by A1,XXREAL_1:234;
then
Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`
)` are_mutually_distinct by A9,A3,A7,A5,A8,A2,A4,Th29,Th31;
hence thesis by BORSUK_5:3;
end;
theorem Th60:
card (Kurat14OpPart KurExSet) = 6
proof
set A = KurExSet;
A1: ( not 5 in ]. -infty, 1 .[)& not 5 in ]. 1, 2 .[ by XXREAL_1:4;
(Cl A)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[ & 5 in (Cl (Cl (Cl A`)`)`)` by Th10
,Th22,BORSUK_5:63,XXREAL_1:235;
then
A2: (Cl A)` <> (Cl (Cl (Cl A`)`)`)` by A1,XBOOLE_0:def 3;
A3: (Cl (Cl (Cl A)`)`)` = ]. -infty, 2 .[ by Th14,TOPMETR:17,XXREAL_1:224,294;
6 in ]. 5,+infty .[ by XXREAL_1:235;
then 6 in (Cl A`)` by Th18,XBOOLE_0:def 3;
then
A4: (Cl (Cl (Cl A)`)`)` <> (Cl A`)` by A3,XXREAL_1:233;
A5: 4 in (Cl (Cl A)`)` by Th13,XXREAL_1:235;
( not 5 in ]. 4, 5 .[)& not 5 in ]. 5,+infty .[ by XXREAL_1:4;
then
A6: not 5 in (Cl A`)` by Th18,XBOOLE_0:def 3;
(Cl A)` <> (Cl Int Cl A)` by Th29,BORSUK_5:71;
then
A7: (Cl A)` <> (Cl (Cl (Cl A)`)`)` by TOPS_1:def 1;
A8: not 5 in (Cl (Cl A`)`)` by Th20,XXREAL_1:233;
(Cl (Cl (Cl A`)`)`)` = ]. 4,+infty .[ by Th21,TOPMETR:17,XXREAL_1:224,288;
then
A9: (Cl (Cl A)`)` <> (Cl (Cl (Cl A`)`)`)` by A5,XXREAL_1:235;
(Cl Int Cl A)` = (Cl (Cl (Cl A)`)`)` & (Cl Int A)` = (Cl (Cl A`)`)` by
TOPS_1:def 1;
then
A10: (Cl (Cl (Cl A)`)`)` <> (Cl (Cl A`)`)` by Th31,BORSUK_5:71;
A11: ( not 5 in (Cl (Cl (Cl A)`)`)`)& 5 in (Cl (Cl (Cl A`)`)`)` by Th15,Th22,
XXREAL_1:233,235;
(Cl (Cl A)`)` <> (Cl (Cl (Cl A)`)`)` by A3,A5,XXREAL_1:233;
then (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`, (Cl A`)`, (Cl (Cl A`)`)`,
(Cl (Cl (Cl A`)`)`)` are_mutually_distinct by A2,A7,A9,A4,A10,A6,A11,A8;
hence thesis by BORSUK_5:3;
end;
theorem Th61:
{ KurExSet, KurExSet` } misses Kurat14ClPart KurExSet
proof
set A = KurExSet;
assume { A, A` } meets Kurat14ClPart A;
then consider x being object such that
A1: x in { A, A` } and
A2: x in Kurat14ClPart A by XBOOLE_0:3;
reconsider x as Subset of R^1 by A2;
x = A or x = A` by A1,TARSKI:def 2;
then
A3: x` = A by A2,TOPS_2:def 2;
x is closed by A2,TOPS_2:def 2;
hence thesis by A3;
end;
registration
cluster KurExSet -> non empty;
coherence;
end;
theorem Th62:
KurExSet <> KurExSet`
by XBOOLE_1:66,XBOOLE_1:79;
theorem Th63:
{ KurExSet, KurExSet` } misses Kurat14OpPart KurExSet
proof
set A = KurExSet;
assume { A, A` } meets Kurat14OpPart A;
then consider x being object such that
A1: x in { A, A` } and
A2: x in Kurat14OpPart A by XBOOLE_0:3;
reconsider x as Subset of R^1 by A2;
x = A or x = A` by A1,TARSKI:def 2;
then
A3: x` = A by A2,TOPS_2:def 1;
x is open by A2,TOPS_2:def 1;
hence thesis by A3;
end;
::$N Kuratowski's closure-complement problem
theorem
card Kurat14Set KurExSet = 14
proof
set A = KurExSet;
set B = { A, A` };
A1: B misses (Kurat14ClPart A \/ Kurat14OpPart A) by Th61,Th63,XBOOLE_1:70;
A2: card (Kurat14ClPart A \/ Kurat14OpPart A) = 6 + 6 by Th57,Th59,Th60,
CARD_2:40
.= 12;
card Kurat14Set A = card (B \/ Kurat14ClPart A \/ Kurat14OpPart A) by Lm2
.= card (B \/ (Kurat14ClPart A \/ Kurat14OpPart A)) by XBOOLE_1:4
.= card B + card (Kurat14ClPart A \/ Kurat14OpPart A) by A1,CARD_2:40
.= 2 + 12 by A2,Th62,CARD_2:57
.= 14;
hence thesis;
end;
begin :: Properties of Kuratowski Sets
definition
let T be TopStruct, A be Subset-Family of T;
attr A is Cl-closed means
for P being Subset of T st P in A holds Cl P in A;
attr A is Int-closed means
for P being Subset of T st P in A holds Int P in A;
end;
registration
let T, A;
cluster Kurat14Set A -> non empty;
coherence;
cluster Kurat14Set A -> Cl-closed;
coherence
by Th6;
cluster Kurat14Set A -> compl-closed;
coherence
proof
for P be Subset of T st P in Kurat14Set A holds P` in Kurat14Set A by Th6;
hence thesis by PROB_1:def 1;
end;
end;
registration
let T, A;
cluster Kurat7Set A -> non empty;
coherence;
cluster Kurat7Set A -> Int-closed;
coherence
by Th9;
cluster Kurat7Set A -> Cl-closed;
coherence
by Th9;
end;
registration
let T;
cluster Int-closed Cl-closed non empty for Subset-Family of T;
existence
proof
take Kurat7Set {}T;
thus thesis;
end;
cluster compl-closed Cl-closed non empty for Subset-Family of T;
existence
proof
take Kurat14Set {}T;
thus thesis;
end;
end;