:: 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
::           (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;


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 :: KURATO_1:1
  A-`-`-`- = A-`-;

definition
  let T, A;
  func Kurat14Part A -> set equals
:: KURATO_1:def 1
  { A, A-, A-`, A-`-, A-`-`, A-`-`-, A-`-`-` };
end;

registration
  let T, A;
  cluster Kurat14Part A -> finite;
end;

definition
  let T, A;
  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`-`-`-` };
end;

theorem :: KURATO_1:2
  Kurat14Set A = Kurat14Part A \/ Kurat14Part A`;

theorem :: KURATO_1:3
  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;

theorem :: KURATO_1:4
  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;

definition
  let T, A;
  func Kurat14ClPart A -> Subset-Family of T equals
:: KURATO_1:def 3
  { A-, A-`-, A-`-`-, A`-, A
  `-`-, A`-`-`- };
  func Kurat14OpPart A -> Subset-Family of T equals
:: KURATO_1:def 4
  { A-`, A-`-`, A-`-`-`, A`-
  `, A`-`-`, A`-`-`-` };
end;

theorem :: KURATO_1:5
  Kurat14Set A = { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A;

registration
  let T, A;
  cluster Kurat14Set A -> finite;
end;

theorem :: KURATO_1:6
  for Q being Subset of T holds Q in Kurat14Set A implies Q` in
  Kurat14Set A & Q- in Kurat14Set A;

theorem :: KURATO_1:7
  card Kurat14Set A <= 14;

begin :: Seven Kuratowski Sets

definition
  let T, A;
  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 };
end;

theorem :: KURATO_1:8
  Kurat7Set A = { A } \/ { Int A, Int Cl A, Int Cl Int A } \/ { Cl A, Cl
  Int A, Cl Int Cl A };

registration
  let T, A;
  cluster Kurat7Set A -> finite;
end;

theorem :: KURATO_1:9
  for Q being Subset of T holds Q in Kurat7Set A implies Int Q in
  Kurat7Set A & Cl Q in Kurat7Set A;

begin :: The Set Generating Exactly Fourteen Kuratowski Sets

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

theorem :: KURATO_1:10
  Cl KurExSet = {1} \/ [. 2,+infty .[;

theorem :: KURATO_1:11
  (Cl KurExSet)` = ]. -infty, 1 .[ \/ ]. 1, 2 .[;

theorem :: KURATO_1:12
  Cl (Cl KurExSet)` = ]. -infty, 2 .];

theorem :: KURATO_1:13
  (Cl (Cl KurExSet)`)` = ]. 2,+infty .[;

theorem :: KURATO_1:14
  Cl (Cl (Cl KurExSet)`)` = [. 2,+infty .[;

theorem :: KURATO_1:15
  (Cl (Cl (Cl KurExSet)`)`)` = ]. -infty, 2 .[;

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

theorem :: KURATO_1:17
  Cl KurExSet` = ]. -infty, 4 .] \/ {5};

theorem :: KURATO_1:18
  (Cl KurExSet`)` = ]. 4, 5 .[ \/ ]. 5,+infty .[;

theorem :: KURATO_1:19
  Cl (Cl KurExSet`)` = [. 4,+infty .[;

theorem :: KURATO_1:20
  (Cl (Cl KurExSet`)`)` = ]. -infty, 4 .[;

theorem :: KURATO_1:21
  Cl (Cl (Cl KurExSet`)`)` = ]. -infty, 4 .];

theorem :: KURATO_1:22
  (Cl (Cl (Cl KurExSet`)`)`)` = ]. 4,+infty .[;

begin :: The Set Generating Exactly Seven Kuratowski Sets

theorem :: KURATO_1:23
  Int KurExSet = ]. 4, 5 .[ \/ ]. 5,+infty .[;

theorem :: KURATO_1:24
  Cl Int KurExSet = [. 4,+infty .[;

theorem :: KURATO_1:25
  Int Cl Int KurExSet = ]. 4,+infty .[;

theorem :: KURATO_1:26
  Int Cl KurExSet = ]. 2,+infty .[;

theorem :: KURATO_1:27
  Cl Int Cl KurExSet = [. 2,+infty .[;

begin :: The Difference Between Chosen Kuratowski Sets

theorem :: KURATO_1:28
  Cl Int Cl KurExSet <> Int Cl KurExSet;

theorem :: KURATO_1:29
  Cl Int Cl KurExSet <> Cl KurExSet;

theorem :: KURATO_1:30
  Cl Int Cl KurExSet <> Int Cl Int KurExSet;

theorem :: KURATO_1:31
  Cl Int Cl KurExSet <> Cl Int KurExSet;

theorem :: KURATO_1:32
  Cl Int Cl KurExSet <> Int KurExSet;

theorem :: KURATO_1:33
  Int Cl KurExSet <> Cl KurExSet;

theorem :: KURATO_1:34
  Int Cl KurExSet <> Int Cl Int KurExSet;

theorem :: KURATO_1:35
  Int Cl KurExSet <> Cl Int KurExSet;

theorem :: KURATO_1:36
  Int Cl KurExSet <> Int KurExSet;

theorem :: KURATO_1:37
  Int Cl Int KurExSet <> Cl KurExSet;

theorem :: KURATO_1:38
  Cl Int KurExSet <> Cl KurExSet;

theorem :: KURATO_1:39
  Int KurExSet <> Cl KurExSet;

theorem :: KURATO_1:40
  Cl KurExSet <> KurExSet;

theorem :: KURATO_1:41
  KurExSet <> Int KurExSet;

theorem :: KURATO_1:42
  Cl Int KurExSet <> Int Cl Int KurExSet;

theorem :: KURATO_1:43
  Int Cl Int KurExSet <> Int KurExSet;

theorem :: KURATO_1:44
  Cl Int KurExSet <> Int KurExSet;

begin :: Final Proofs For Seven

theorem :: KURATO_1:45
  Int Cl Int KurExSet <> Int Cl KurExSet;

theorem :: KURATO_1:46
  Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet are_mutually_distinct;

theorem :: KURATO_1:47
  Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct;

theorem :: KURATO_1:48
  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;

theorem :: KURATO_1:49
  for X being set st X in { Int KurExSet, Int Cl KurExSet, Int Cl
  Int KurExSet } holds X <> REAL;

theorem :: KURATO_1:50
  for X being set st X in { Cl KurExSet, Cl Int KurExSet, Cl Int Cl
  KurExSet } holds X <> REAL;

theorem :: KURATO_1:51
  { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet } misses {
  Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };

theorem :: KURATO_1:52
  Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet, Cl KurExSet,
  Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_distinct;

registration
  cluster KurExSet -> non closed non open;
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 };

theorem :: 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;

theorem :: KURATO_1:55
  card Kurat7Set KurExSet = 7;

begin :: Final Proofs For Fourteen

registration
  cluster Kurat14ClPart KurExSet -> with_proper_subsets;
  cluster Kurat14OpPart KurExSet -> with_proper_subsets;
end;

registration
  cluster Kurat14Set KurExSet -> with_proper_subsets;
end;

registration
  cluster Kurat14Set KurExSet -> with_non-empty_elements;
end;

theorem :: KURATO_1:56
  for A being with_non-empty_elements set, B being set st B c= A
  holds B is with_non-empty_elements;

registration
  cluster Kurat14ClPart KurExSet -> with_non-empty_elements;
  cluster Kurat14OpPart KurExSet -> with_non-empty_elements;
end;

registration
  cluster with_proper_subsets with_non-empty_elements for Subset-Family of R^1;
end;

theorem :: KURATO_1:57
  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;

registration
  cluster Kurat14ClPart KurExSet -> closed;
  cluster Kurat14OpPart KurExSet -> open;
end;

theorem :: KURATO_1:58
  Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet;

registration
  let T, A;
  cluster Kurat14ClPart A -> finite;
  cluster Kurat14OpPart A -> finite;
end;

theorem :: KURATO_1:59
  card (Kurat14ClPart KurExSet) = 6;

theorem :: KURATO_1:60
  card (Kurat14OpPart KurExSet) = 6;

theorem :: KURATO_1:61
  { KurExSet, KurExSet` } misses Kurat14ClPart KurExSet;

registration
  cluster KurExSet -> non empty;
end;

theorem :: KURATO_1:62
  KurExSet <> KurExSet`;

theorem :: KURATO_1:63
  { KurExSet, KurExSet` } misses Kurat14OpPart KurExSet;

::$N Kuratowski's closure-complement problem
theorem :: KURATO_1:64
  card Kurat14Set KurExSet = 14;

begin :: Properties of Kuratowski Sets

definition
  let T be TopStruct, 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;

registration
  let T, A;
  cluster Kurat14Set A -> non empty;
  cluster Kurat14Set A -> Cl-closed;
  cluster Kurat14Set A -> compl-closed;
end;

registration
  let T, A;
  cluster Kurat7Set A -> non empty;
  cluster Kurat7Set A -> Int-closed;
  cluster Kurat7Set A -> Cl-closed;
end;

registration
  let T;
  cluster Int-closed Cl-closed non empty for Subset-Family of T;
  cluster compl-closed Cl-closed non empty for Subset-Family of T;
end;