:: On the {K}uratowski Closure-Complement Problem
:: by Lilla Krystyna Bagi\'nska and Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

notation

let T be non empty TopSpace;
let A be Subset of T;
synonym A - for Cl A;

end;

theorem Th1: :: KURATO_1:1

for T being non empty TopSpace
for A being Subset of T holds ((((((A -) `) -) `) -) `) - = ((A -) `) -

proof end;

Lm1: for T being 1-sorted
for A, B being Subset-Family of T holds A \/ B is Subset-Family of T
;

definition

let T be non empty TopSpace;
let A be Subset of T;

func Kurat14Part A -> set equals :: KURATO_1:def 1
{A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)};

coherence
{A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} is set ;

end;

:: deftheorem defines Kurat14Part KURATO_1:def 1 :
for T being non empty TopSpace
for A being Subset of T holds Kurat14Part A = {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)};

registration

let T be non empty TopSpace;
let A be Subset of T;

cluster Kurat14Part A -> finite ;

coherence
Kurat14Part A is finite ;

end;

definition

let T be non empty TopSpace;
let A be Subset of T;

func Kurat14Set A -> Subset-Family of T equals :: KURATO_1:def 2
{A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)};

coherence
{A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T

proof end;

end;

:: deftheorem defines Kurat14Set KURATO_1:def 2 :
for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)};

theorem :: KURATO_1:2

for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = (Kurat14Part A) \/ (Kurat14Part (A `)) ;

theorem Th3: :: KURATO_1:3

for T being non empty TopSpace
for A being Subset of T holds
( 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 end;

theorem Th4: :: KURATO_1:4

for T being non empty TopSpace
for A being Subset of T holds
( 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 end;

definition

let T be non empty TopSpace;
let A be Subset of T;

func Kurat14ClPart A -> Subset-Family of T equals :: KURATO_1:def 3
{(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)};

coherence
{(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)} is Subset-Family of T

proof end;

func Kurat14OpPart A -> Subset-Family of T equals :: KURATO_1:def 4
{((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)};

coherence
{((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T

proof end;

end;

:: deftheorem defines Kurat14ClPart KURATO_1:def 3 :
for T being non empty TopSpace
for A being Subset of T holds Kurat14ClPart A = {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)};

:: deftheorem defines Kurat14OpPart KURATO_1:def 4 :
for T being non empty TopSpace
for A being Subset of T holds Kurat14OpPart A = {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)};

Lm2: for T being non empty TopSpace
for A being Subset of T holds 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 end;

theorem :: KURATO_1:5

for T being non empty TopSpace
for A being Subset of T holds Kurat14Set A = ({A,(A `)} \/ (Kurat14ClPart A)) \/ (Kurat14OpPart A) by Lm2;

registration

let T be non empty TopSpace;
let A be Subset of T;

cluster Kurat14Set A -> finite ;

coherence
Kurat14Set A is finite ;

end;

theorem Th6: :: KURATO_1:6

for T being non empty TopSpace
for A, Q being Subset of T st Q in Kurat14Set A holds
( Q ` in Kurat14Set A & Q - in Kurat14Set A )

proof end;

theorem :: KURATO_1:7

for T being non empty TopSpace
for A being Subset of T holds card (Kurat14Set A) <= 14

proof end;

definition

let T be non empty TopSpace;
let A be Subset of T;

func Kurat7Set A -> Subset-Family of T equals :: KURATO_1:def 5
{A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))};

coherence
{A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} is Subset-Family of T

proof end;

end;

:: deftheorem defines Kurat7Set KURATO_1:def 5 :
for T being non empty TopSpace
for A being Subset of T holds Kurat7Set A = {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))};

theorem :: KURATO_1:8

for T being non empty TopSpace
for A being Subset of T holds Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))}

proof end;

registration

let T be non empty TopSpace;
let A be Subset of T;

cluster Kurat7Set A -> finite ;

coherence
Kurat7Set A is finite ;

end;

theorem Th9: :: KURATO_1:9

for T being non empty TopSpace
for A, Q being Subset of T st Q in Kurat7Set A holds
( Int Q in Kurat7Set A & Cl Q in Kurat7Set A )

proof end;

definition

func KurExSet -> Subset of R^1 equals :: KURATO_1:def 6
(({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[;

coherence
(({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[ is Subset of R^1 by TOPMETR:17;

end;

:: deftheorem defines KurExSet KURATO_1:def 6 :
KurExSet = (({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[;

theorem Th10: :: KURATO_1:10

Cl KurExSet = {1} \/ [.2,+infty.[

proof end;

theorem Th11: :: KURATO_1:11

(Cl KurExSet) ` = ].-infty,1.[ \/ ].1,2.[ by Th10, BORSUK_5:63;

theorem Th12: :: KURATO_1:12

Cl ((Cl KurExSet) `) = ].-infty,2.] by Th11, BORSUK_5:64;

theorem Th13: :: KURATO_1:13

(Cl ((Cl KurExSet) `)) ` = ].2,+infty.[ by Th12, TOPMETR:17, XXREAL_1:224, XXREAL_1:288;

theorem Th14: :: KURATO_1:14

Cl ((Cl ((Cl KurExSet) `)) `) = [.2,+infty.[ by Th13, BORSUK_5:49;

theorem Th15: :: KURATO_1:15

(Cl ((Cl ((Cl KurExSet) `)) `)) ` = ].-infty,2.[ by Th14, TOPMETR:17, XXREAL_1:224, XXREAL_1:294;

theorem Th16: :: KURATO_1:16

KurExSet ` = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5}

proof end;

theorem Th17: :: KURATO_1:17

Cl (KurExSet `) = ].-infty,4.] \/ {5} by Th16, BORSUK_5:67;

theorem Th18: :: KURATO_1:18

(Cl (KurExSet `)) ` = ].4,5.[ \/ ].5,+infty.[ by Th17, BORSUK_5:68;

theorem Th19: :: KURATO_1:19

Cl ((Cl (KurExSet `)) `) = [.4,+infty.[ by Th18, BORSUK_5:55;

theorem Th20: :: KURATO_1:20

(Cl ((Cl (KurExSet `)) `)) ` = ].-infty,4.[ by Th19, TOPMETR:17, XXREAL_1:224, XXREAL_1:294;

theorem Th21: :: KURATO_1:21

Cl ((Cl ((Cl (KurExSet `)) `)) `) = ].-infty,4.] by Th20, BORSUK_5:51;

theorem Th22: :: KURATO_1:22

(Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` = ].4,+infty.[ by Th21, TOPMETR:17, XXREAL_1:224, XXREAL_1:288;

theorem Th23: :: KURATO_1:23

Int KurExSet = ].4,5.[ \/ ].5,+infty.[ by Th18, TOPS_1:def 1;

theorem Th24: :: KURATO_1:24

Cl (Int KurExSet) = [.4,+infty.[ by Th18, BORSUK_5:55, TOPS_1:def 1;

theorem Th25: :: KURATO_1:25

Int (Cl (Int KurExSet)) = ].4,+infty.[

proof end;

theorem Th26: :: KURATO_1:26

Int (Cl KurExSet) = ].2,+infty.[

proof end;

theorem Th27: :: KURATO_1:27

Cl (Int (Cl KurExSet)) = [.2,+infty.[

proof end;

theorem :: KURATO_1:28

Cl (Int (Cl KurExSet)) <> Int (Cl KurExSet) by Th27, XXREAL_1:236, Th26, XXREAL_1:235;

theorem Th29: :: KURATO_1:29

Cl (Int (Cl KurExSet)) <> Cl KurExSet

proof end;

theorem :: KURATO_1:30

Cl (Int (Cl KurExSet)) <> Int (Cl (Int KurExSet)) by Th27, XXREAL_1:236, Th25, XXREAL_1:235;

theorem Th31: :: KURATO_1:31

Cl (Int (Cl KurExSet)) <> Cl (Int KurExSet)

proof end;

theorem :: KURATO_1:32

Cl (Int (Cl KurExSet)) <> Int KurExSet

proof end;

theorem :: KURATO_1:33

Int (Cl KurExSet) <> Cl KurExSet

proof end;

theorem :: KURATO_1:34

Int (Cl KurExSet) <> Int (Cl (Int KurExSet))

proof end;

theorem :: KURATO_1:35

Int (Cl KurExSet) <> Cl (Int KurExSet) by Th26, BORSUK_5:34, BORSUK_5:45;

theorem Th36: :: KURATO_1:36

Int (Cl KurExSet) <> Int KurExSet

proof end;

theorem :: KURATO_1:37

Int (Cl (Int KurExSet)) <> Cl KurExSet

proof end;

theorem Th38: :: KURATO_1:38

Cl (Int KurExSet) <> Cl KurExSet

proof end;

theorem :: KURATO_1:39

Int KurExSet <> Cl KurExSet

proof end;

theorem Th40: :: KURATO_1:40

Cl KurExSet <> KurExSet

proof end;

theorem Th41: :: KURATO_1:41

KurExSet <> Int KurExSet

proof end;

theorem :: KURATO_1:42

Cl (Int KurExSet) <> Int (Cl (Int KurExSet)) by Th24, XXREAL_1:236, Th25, XXREAL_1:235;

theorem Th43: :: KURATO_1:43

Int (Cl (Int KurExSet)) <> Int KurExSet

proof end;

theorem :: KURATO_1:44

Cl (Int KurExSet) <> Int KurExSet

proof end;

theorem Th45: :: KURATO_1:45

Int (Cl (Int KurExSet)) <> Int (Cl KurExSet)

proof end;

theorem Th46: :: KURATO_1:46

Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)) are_mutually_distinct by Th36, Th43, Th45;

theorem Th47: :: KURATO_1:47

Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_distinct by Th38, Th29, Th31;

theorem Th48: :: KURATO_1:48

for X being set st X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} holds
X is non empty open Subset of R^1

proof end;

theorem Th49: :: KURATO_1:49

for X being set st X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} holds
X <> REAL

proof end;

theorem :: KURATO_1:50

for X being set st X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} holds
X <> REAL

proof end;

theorem Th51: :: KURATO_1:51

{(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} misses {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))}

proof end;

theorem Th52: :: KURATO_1:52

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 open non closed ;

coherence
( not KurExSet is closed & not KurExSet is open ) by Th40, Th41, PRE_TOPC:22, TOPS_1:23;

end;

theorem :: KURATO_1:53

{(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet))),(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} misses {KurExSet}

proof end;

theorem Th54: :: KURATO_1:54

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 :: KURATO_1:55

card (Kurat7Set KurExSet) = 7

proof end;

registration

cluster Kurat14ClPart KurExSet -> with_proper_subsets ;

coherence
Kurat14ClPart KurExSet is with_proper_subsets

proof end;

cluster Kurat14OpPart KurExSet -> with_proper_subsets ;

coherence
Kurat14OpPart KurExSet is with_proper_subsets

proof end;

end;

registration

cluster Kurat14Set KurExSet -> with_proper_subsets ;

coherence
Kurat14Set KurExSet is with_proper_subsets

proof end;

end;

registration

cluster Kurat14Set KurExSet -> with_non-empty_elements ;

coherence
Kurat14Set KurExSet is with_non-empty_elements

proof end;

end;

theorem Th56: :: KURATO_1:56

for A being with_non-empty_elements set
for B being set st B c= A holds
B is with_non-empty_elements

proof end;

registration

cluster Kurat14ClPart KurExSet -> with_non-empty_elements ;

coherence
Kurat14ClPart KurExSet is with_non-empty_elements

proof end;

cluster Kurat14OpPart KurExSet -> with_non-empty_elements ;

coherence
Kurat14OpPart KurExSet is with_non-empty_elements

proof end;

end;

registration

cluster with_non-empty_elements with_proper_subsets for Element of bool (bool the carrier of R^1);

existence
ex b₁ being Subset-Family of R^1 st
( b₁ is with_proper_subsets & b₁ is with_non-empty_elements )

proof end;

end;

theorem Th57: :: KURATO_1:57

for F, G being with_non-empty_elements with_proper_subsets Subset-Family of R^1 st F is open & G is closed holds
F misses G

proof end;

registration

cluster Kurat14ClPart KurExSet -> closed ;

coherence
Kurat14ClPart KurExSet is closed by ENUMSET1:def 4;

cluster Kurat14OpPart KurExSet -> open ;

coherence
Kurat14OpPart KurExSet is open by ENUMSET1:def 4;

end;

theorem :: KURATO_1:58

Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th57;

registration

let T be non empty TopSpace;
let A be Subset of T;

cluster Kurat14ClPart A -> finite ;

coherence
Kurat14ClPart A is finite ;

cluster Kurat14OpPart A -> finite ;

coherence
Kurat14OpPart A is finite ;

end;

theorem Th59: :: KURATO_1:59

card (Kurat14ClPart KurExSet) = 6

proof end;

theorem Th60: :: KURATO_1:60

card (Kurat14OpPart KurExSet) = 6

proof end;

theorem Th61: :: KURATO_1:61

{KurExSet,(KurExSet `)} misses Kurat14ClPart KurExSet

proof end;

registration

cluster KurExSet -> non empty ;

coherence
not KurExSet is empty ;

end;

theorem Th62: :: KURATO_1:62

KurExSet <> KurExSet ` by XBOOLE_1:66, XBOOLE_1:79;

theorem Th63: :: KURATO_1:63

{KurExSet,(KurExSet `)} misses Kurat14OpPart KurExSet

proof end;

:: Kuratowski's closure-complement problem

theorem :: KURATO_1:64

card (Kurat14Set KurExSet) = 14

proof end;

definition

let T be TopStruct ;
let A be Subset-Family of T;

attr A is Cl-closed means :: KURATO_1:def 7
for P being Subset of T st P in A holds
Cl P in A;

attr A is Int-closed means :: KURATO_1:def 8
for P being Subset of T st P in A holds
Int P in A;

end;

:: deftheorem defines Cl-closed KURATO_1:def 7 :
for T being TopStruct
for A being Subset-Family of T holds
( A is Cl-closed iff for P being Subset of T st P in A holds
Cl P in A );

:: deftheorem defines Int-closed KURATO_1:def 8 :
for T being TopStruct
for A being Subset-Family of T holds
( A is Int-closed iff for P being Subset of T st P in A holds
Int P in A );

registration

let T be non empty TopSpace;
let A be Subset of T;

cluster Kurat14Set A -> non empty ;

coherence
not Kurat14Set A is empty ;

cluster Kurat14Set A -> Cl-closed ;

coherence
Kurat14Set A is Cl-closed by Th6;

cluster Kurat14Set A -> compl-closed ;

coherence
Kurat14Set A is compl-closed

proof end;

end;

registration

let T be non empty TopSpace;
let A be Subset of T;

cluster Kurat7Set A -> non empty ;

coherence
not Kurat7Set A is empty ;

cluster Kurat7Set A -> Int-closed ;

coherence
Kurat7Set A is Int-closed by Th9;

cluster Kurat7Set A -> Cl-closed ;

coherence
Kurat7Set A is Cl-closed by Th9;

end;

registration

let T be non empty TopSpace;

cluster non empty Cl-closed Int-closed for Element of bool (bool the carrier of T);

existence
ex b₁ being Subset-Family of T st
( b₁ is Int-closed & b₁ is Cl-closed & not b₁ is empty )

proof end;

cluster non empty compl-closed Cl-closed for Element of bool (bool the carrier of T);

existence
ex b₁ being Subset-Family of T st
( b₁ is compl-closed & b₁ is Cl-closed & not b₁ is empty )

proof end;

end;