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

begin

notation

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

end;

theorem Th1: :: KURATO_1:1

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

proof end;

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

definition

let T be non empty TopSpace;
let A be Subset of ;
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 holds Kurat14Part A = {A,(A - ),((A - ) ` ),(((A - ) ` ) - ),((((A - ) ` ) - ) ` ),(((((A - ) ` ) - ) ` ) - ),((((((A - ) ` ) - ) ` ) - ) ` )};

registration

let T be non empty TopSpace;
let A be Subset of ;
cluster Kurat14Part A -> finite ;
coherence
Kurat14Part A is finite ;

end;

definition

let T be non empty TopSpace;
let A be Subset of ;
func Kurat14Set A -> Subset-Family of 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

proof end;

end;

:: deftheorem defines Kurat14Set KURATO_1:def 2 :

for T being non empty TopSpace
for A being Subset of 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 holds Kurat14Set A = (Kurat14Part A) \/ (Kurat14Part (A ` )) ;

theorem Th3: :: KURATO_1:3

for T being non empty TopSpace
for A being Subset of 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 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 ;
func Kurat14ClPart A -> Subset-Family of equals :: KURATO_1:def 3
{(A - ),(((A - ) ` ) - ),(((((A - ) ` ) - ) ` ) - ),((A ` ) - ),((((A ` ) - ) ` ) - ),((((((A ` ) - ) ` ) - ) ` ) - )};
coherence
{(A - ),(((A - ) ` ) - ),(((((A - ) ` ) - ) ` ) - ),((A ` ) - ),((((A ` ) - ) ` ) - ),((((((A ` ) - ) ` ) - ) ` ) - )} is Subset-Family of

proof end;

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

proof end;

end;

:: deftheorem defines Kurat14ClPart KURATO_1:def 3 :

for T being non empty TopSpace
for A being Subset of 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 holds Kurat14OpPart A = {((A - ) ` ),((((A - ) ` ) - ) ` ),((((((A - ) ` ) - ) ` ) - ) ` ),(((A ` ) - ) ` ),(((((A ` ) - ) ` ) - ) ` ),(((((((A ` ) - ) ` ) - ) ` ) - ) ` )};

Lm2: for T being non empty TopSpace
for A being Subset of 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 holds Kurat14Set A = ({A,(A ` )} \/ (Kurat14ClPart A)) \/ (Kurat14OpPart A) by Lm2;

registration

let T be non empty TopSpace;
let A be Subset of ;
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 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 holds card (Kurat14Set A) <= 14

proof end;

begin

definition

let T be non empty TopSpace;
let A be Subset of ;
func Kurat7Set A -> Subset-Family of 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

proof end;

end;

:: deftheorem defines Kurat7Set KURATO_1:def 5 :

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

canceled;

theorem :: KURATO_1:9

for T being non empty TopSpace
for A being Subset of 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 ;
cluster Kurat7Set A -> finite ;
coherence
Kurat7Set A is finite ;

end;

theorem Th10: :: KURATO_1:10

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

proof end;

begin

definition

func KurExSet -> Subset of 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 by TOPMETR:24;

end;

:: deftheorem defines KurExSet KURATO_1:def 6 :

KurExSet = (({1} \/ (RAT 2,4)) \/ ].4,5.[) \/ ].5,+infty .[;

theorem :: KURATO_1:11

canceled;

theorem Th12: :: KURATO_1:12

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

proof end;

theorem Th13: :: KURATO_1:13

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

theorem Th14: :: KURATO_1:14

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

theorem Th15: :: KURATO_1:15

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

theorem Th16: :: KURATO_1:16

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

theorem Th17: :: KURATO_1:17

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

theorem Th18: :: KURATO_1:18

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

proof end;

theorem Th19: :: KURATO_1:19

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

theorem Th20: :: KURATO_1:20

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

theorem Th21: :: KURATO_1:21

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

theorem Th22: :: KURATO_1:22

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

theorem Th23: :: KURATO_1:23

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

theorem Th24: :: KURATO_1:24

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

begin

theorem Th25: :: KURATO_1:25

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

theorem Th26: :: KURATO_1:26

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

theorem Th27: :: KURATO_1:27

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

proof end;

theorem Th28: :: KURATO_1:28

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

proof end;

theorem Th29: :: KURATO_1:29

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

proof end;

begin

theorem :: KURATO_1:30

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

proof end;

theorem Th31: :: KURATO_1:31

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

proof end;

theorem :: KURATO_1:32

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

proof end;

theorem Th33: :: KURATO_1:33

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

proof end;

theorem :: KURATO_1:34

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

proof end;

theorem :: KURATO_1:35

Int (Cl KurExSet ) <> Cl KurExSet

proof end;

theorem :: KURATO_1:36

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

proof end;

theorem :: KURATO_1:37

Int (Cl KurExSet ) <> Cl (Int KurExSet ) by Th28, BORSUK_5:57, BORSUK_5:71;

theorem Th38: :: KURATO_1:38

Int (Cl KurExSet ) <> Int KurExSet

proof end;

theorem :: KURATO_1:39

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

proof end;

theorem Th40: :: KURATO_1:40

Cl (Int KurExSet ) <> Cl KurExSet

proof end;

theorem :: KURATO_1:41

Int KurExSet <> Cl KurExSet

proof end;

theorem Th42: :: KURATO_1:42

Cl KurExSet <> KurExSet

proof end;

theorem Th43: :: KURATO_1:43

KurExSet <> Int KurExSet

proof end;

theorem :: KURATO_1:44

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

proof end;

theorem Th45: :: KURATO_1:45

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

proof end;

theorem :: KURATO_1:46

Cl (Int KurExSet ) <> Int KurExSet

proof end;

begin

theorem Th47: :: KURATO_1:47

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

proof end;

theorem Th48: :: KURATO_1:48

Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )) are_mutually_different

proof end;

theorem Th49: :: KURATO_1:49

Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different

proof end;

theorem Th50: :: KURATO_1:50

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

proof end;

theorem :: KURATO_1:51

canceled;

theorem Th52: :: KURATO_1:52

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

proof end;

theorem :: KURATO_1:53

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

proof end;

theorem Th54: :: KURATO_1:54

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

proof end;

theorem Th55: :: KURATO_1:55

Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )), Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different by Th48, Th49, Th54, BORSUK_5:7;

registration

cluster KurExSet -> non open non closed ;
coherence
( not KurExSet is closed & not KurExSet is open ) by Th42, Th43, PRE_TOPC:52, TOPS_1:55;

end;

theorem Th56: :: KURATO_1:56

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

proof end;

theorem Th57: :: KURATO_1:57

KurExSet , Int KurExSet , Int (Cl KurExSet ), Int (Cl (Int KurExSet )), Cl KurExSet , Cl (Int KurExSet ), Cl (Int (Cl KurExSet )) are_mutually_different

proof end;

theorem :: KURATO_1:58

card (Kurat7Set KurExSet ) = 7

proof end;

begin

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 Th59: :: KURATO_1:59

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 Element of bool (bool the carrier of R^1 );
existence
ex b₁ being Subset-Family of st
( b₁ is with_proper_subsets & b₁ is with_non-empty_elements )

proof end;

end;

theorem Th60: :: KURATO_1:60

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

proof end;

registration

cluster Kurat14ClPart KurExSet -> closed ;
coherence
Kurat14ClPart KurExSet is closed

proof end;

cluster Kurat14OpPart KurExSet -> open ;
coherence
Kurat14OpPart KurExSet is open

proof end;

end;

theorem :: KURATO_1:61

Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th60;

registration

let T be non empty TopSpace;
let A be Subset of ;
cluster Kurat14ClPart A -> finite ;
coherence
Kurat14ClPart A is finite ;
cluster Kurat14OpPart A -> finite ;
coherence
Kurat14OpPart A is finite ;

end;

theorem Th62: :: KURATO_1:62

card (Kurat14ClPart KurExSet ) = 6

proof end;

theorem Th63: :: KURATO_1:63

card (Kurat14OpPart KurExSet ) = 6

proof end;

theorem Th64: :: KURATO_1:64

{KurExSet ,(KurExSet ` )} misses Kurat14ClPart KurExSet

proof end;

registration

cluster KurExSet -> non empty ;
coherence
not KurExSet is empty ;

end;

theorem Th65: :: KURATO_1:65

KurExSet <> KurExSet `

proof end;

theorem Th66: :: KURATO_1:66

{KurExSet ,(KurExSet ` )} misses Kurat14OpPart KurExSet

proof end;

theorem :: KURATO_1:67

card (Kurat14Set KurExSet ) = 14

proof end;

begin

definition

let T be TopStruct ;
let A be Subset-Family of ;
attr A is Cl-closed means :: KURATO_1:def 7
for P being Subset of st P in A holds
Cl P in A;
attr A is Int-closed means :: KURATO_1:def 8
for P being Subset of 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 holds
( A is Cl-closed iff for P being Subset of 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 holds
( A is Int-closed iff for P being Subset of st P in A holds
Int P in A );

registration

let T be non empty TopSpace;
let A be Subset of ;
cluster Kurat14Set A -> non empty ;
coherence
not Kurat14Set A is empty ;
cluster Kurat14Set A -> Cl-closed ;
coherence
Kurat14Set A is Cl-closed

proof end;

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 ;
cluster Kurat7Set A -> non empty ;
coherence
not Kurat7Set A is empty ;
cluster Kurat7Set A -> Int-closed ;
coherence
Kurat7Set A is Int-closed

proof end;

cluster Kurat7Set A -> Cl-closed ;
coherence
Kurat7Set A is Cl-closed

proof end;

end;

registration

let T be non empty TopSpace;
cluster non empty Cl-closed Int-closed Element of bool (bool the carrier of T);
existence
ex b₁ being Subset-Family of st
( b₁ is Int-closed & b₁ is Cl-closed & not b₁ is empty )

proof end;

cluster non empty compl-closed Cl-closed Element of bool (bool the carrier of T);
existence
ex b₁ being Subset-Family of st
( b₁ is compl-closed & b₁ is Cl-closed & not b₁ is empty )

proof end;

end;