:: Stone Lattices
::  by Adam Grabowski
::
:: Received October 22, 2015
:: Copyright (c) 2015-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 SUBSET_1, LATTICES, LATSTONE, XBOOLE_0, TARSKI, EQREL_1, PBOOLE,
      ORDINAL4, XXREAL_2, STRUCT_0, ZFMISC_1, LATTICE5, FILTER_0, LATTICE4,
      TOPS_1, REWRITE1, MOEBIUS2, NAT_1, FINSET_1, XCMPLX_0, MOEBIUS1, RELAT_1,
      BINOP_1, REALSET1, LATTICEA, XXREAL_0, CARD_1, NUMBERS, NEWTON, ARYTM_3;
 notations TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, ORDINAL1, NAT_1, FINSET_1,
      ARYTM_3, BINOP_1, REALSET1, SUBSET_1, NAT_D, ENUMSET1, XCMPLX_0,
      XXREAL_0, CARD_1, NUMBERS, NEWTON, INT_2, FUNCT_1, FUNCT_2, STRUCT_0,
      LATTICES, LATTICE3, FILTER_0, FILTER_1, FILTER_2, LATTICE4, MOEBIUS1,
      MOEBIUS2, LATTICEA;
 constructors DOMAIN_1, XBOOLE_0, FILTER_1, NAT_1, ORDINAL1, INT_2, NEWTON,
      ARYTM_3, NAT_D, SQUARE_1, ENUMSET1, ZFMISC_1, FILTER_0, FINSET_1,
      FILTER_2, LATTICE4, MOEBIUS1, XREAL_0, XCMPLX_0, XXREAL_0, BINOP_1,
      REALSET2, LATTICE3, PARTFUN1, MOEBIUS2, SUBSET_1, BOOLEALG, REALSET1,
      LATTICEA;
 registrations STRUCT_0, LATTICES, INT_1, FILTER_1, MOEBIUS1, MOEBIUS2,
      XCMPLX_0, INT_3, NEWTON, NAT_1, ORDINAL1, XXREAL_0, RELSET_1, LATTICE6;
 requirements SUBSET, BOOLE, REAL, NUMERALS;


begin :: Preliminaries

:: The main aim of this article is to provide a formal counterpart
:: for the paper of Jouni J\"arvinen "Lattice theory for rough sets",
:: in Transactions of Rough Sets, VI, LNCS vol. 4374, pp. 400--498, 2007.
:: The corresponding items are marked by the acronym LTRS. We deal
:: with Section 4.3, page 423--426.

theorem :: LATSTONE:1
  for L being distributive Lattice, S being Sublattice of L holds
    S is distributive;

registration let L be distributive Lattice;
  cluster -> distributive for Sublattice of L;
end;

registration let L1, L2 be bounded Lattice;
  cluster [:L1,L2:] -> bounded;
end;

 reserve L for Lattice;
 reserve I,P for non empty ClosedSubset of L;

theorem :: LATSTONE:2
  L is lower-bounded & Bottom L in I implies latt (L,I) is lower-bounded
    & Bottom latt (L,I) = Bottom L;

theorem :: LATSTONE:3
  L is upper-bounded & Top L in I implies latt (L,I) is upper-bounded
    & Top latt (L,I) = Top L;

begin :: Pseudocomplements in Lattices

::$N Pseudocomplement

definition let L be non empty LattStr;
  let a,b be Element of L;
  pred a is_a_pseudocomplement_of b means
:: LATSTONE:def 1
    a "/\" b = Bottom L &
    for x being Element of L st b "/\" x = Bottom L holds x [= a;
end;

:: p. 122 6.1 Definition from Gratzer

definition let L be non empty LattStr;
  attr L is pseudocomplemented means
:: LATSTONE:def 2
    for x being Element of L
    ex y being Element of L st y is_a_pseudocomplement_of x;
end;

:: LTRS: Example 43(a)

theorem :: LATSTONE:4
  for L being Boolean Lattice holds L is pseudocomplemented;

registration
  cluster Boolean -> pseudocomplemented for Lattice;
end;

registration
  cluster Boolean pseudocomplemented bounded for Lattice;
end;

:: Pseudocomplements are unique

theorem :: LATSTONE:5
  for L being pseudocomplemented lower-bounded Lattice,
  a, b, x being Element of L st a is_a_pseudocomplement_of x &
    b is_a_pseudocomplement_of x holds a = b;

:: The unique pseudocomplement

definition let L be non empty LattStr, x be Element of L;
  assume L is pseudocomplemented lower-bounded Lattice;
  func x* -> Element of L means
:: LATSTONE:def 3
    it is_a_pseudocomplement_of x;
end;

theorem :: LATSTONE:6
  for L being pseudocomplemented lower-bounded Lattice, x being Element of L
  holds x* "/\" x = Bottom L;

reserve L for lower-bounded pseudocomplemented Lattice;

:: LTRS: Lemma 42(a)

theorem :: LATSTONE:7
  for a being Element of L holds a [= a**;

:: LTRS: Lemma 42(b)

theorem :: LATSTONE:8
  for a, b being Element of L holds a [= b implies b* [= a*;

:: LTRS: Lemma 42(c)

theorem :: LATSTONE:9
  for a being Element of L holds a* = a***;

:: LTRS: Example 43(c)
theorem :: LATSTONE:10
  for L being pseudocomplemented bounded Lattice holds (Bottom L)* = Top L;

:: LTRS: Example 43(c)
theorem :: LATSTONE:11
  for L being pseudocomplemented bounded Lattice holds (Top L)* = Bottom L;

:: Pseudocomplements are precisely complements in complemented lattices.
:: A complement (if exists) is always a pseudocomplement.

:: LTRS: Example 43(a)
theorem :: LATSTONE:12
  for L being Boolean Lattice, x being Element of L holds x` = x*;

:: Connection between pseudocomplements and the functor from LATTICEA

theorem :: LATSTONE:13
  for L being pseudocomplemented bounded Lattice, x, y being Element of L st
    y is_a_pseudocomplement_of x holds y in PseudoComplements x;

theorem :: LATSTONE:14
  for L being pseudocomplemented bounded Lattice, x being Element of L holds
    x* in PseudoComplements x;

begin :: Skeleton of a Pseudocomplemented Lattice

definition let L be lower-bounded pseudocomplemented Lattice;
  func Skeleton L -> Subset of L equals
:: LATSTONE:def 4
    the set of all a* where a is Element of L;
end;

theorem :: LATSTONE:15
  for L being lower-bounded pseudocomplemented Lattice holds
    Skeleton L = { a where a is Element of L : a** = a };

:: LTRS: Lemma 44(a), p. 424

theorem :: LATSTONE:16
  for L being lower-bounded pseudocomplemented Lattice, x being Element of L
  holds x in Skeleton L iff x** = x;

registration let L be bounded pseudocomplemented Lattice;
  cluster Skeleton L -> non empty;
end;

theorem :: LATSTONE:17
  for L being pseudocomplemented distributive lower-bounded Lattice holds
  for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
  a "/\" b in Skeleton L;

begin :: Stone Identity

definition let L be non empty LattStr;
  attr L is satisfying_Stone_identity means
:: LATSTONE:def 5
    for x being Element of L holds x* "\/" (x**) = Top L;
end;

theorem :: LATSTONE:18
  for L being Boolean Lattice holds L is satisfying_Stone_identity;

registration
  cluster Boolean -> satisfying_Stone_identity for Lattice;
end;

registration
  cluster satisfying_Stone_identity pseudocomplemented Boolean for Lattice;
end;

:: LTRS: Lemma 44(b), p. 424

theorem :: LATSTONE:19
  for L being pseudocomplemented distributive bounded Lattice holds
    L is satisfying_Stone_identity iff for a, b being Element of L holds
      (a "/\" b)* = (a*) "\/" (b*);

::$N Stone algebra

definition
  let L be Lattice;
  attr L is Stone means
:: LATSTONE:def 6
    L is pseudocomplemented distributive bounded satisfying_Stone_identity;
end;

registration
  cluster Stone ->
    pseudocomplemented distributive bounded satisfying_Stone_identity
      for Lattice;
  cluster pseudocomplemented distributive bounded satisfying_Stone_identity
      -> Stone for Lattice;
end;

:: LTRS:

theorem :: LATSTONE:20
  for L being pseudocomplemented distributive bounded Lattice holds
    L is satisfying_Stone_identity iff for a, b being Element of L st
    a in Skeleton L & b in Skeleton L holds a "\/" b in Skeleton L;

reserve L for Stone Lattice;

:: LTRS: Proposition 45

theorem :: LATSTONE:21
  Top L in Skeleton L & Bottom L in Skeleton L;

definition let L be Stone Lattice, a be Element of L;
  attr a is skeletal means
:: LATSTONE:def 7
    a in Skeleton L;
end;

registration
  let L be Stone Lattice;
  cluster Top L -> skeletal;
  cluster Bottom L -> skeletal;
end;

:: LTRS: Proposition 45

registration let L be Stone Lattice;
  cluster Skeleton L -> join-closed meet-closed;
end;

definition let L be Stone Lattice;
  redefine func Skeleton L -> ClosedSubset of L;
end;

:: Skeleton equipped with the lattice structure

definition let L be Stone Lattice;
  func SkelLatt L -> Sublattice of L equals
:: LATSTONE:def 8
  latt (L,Skeleton L);
end;

registration let L be Stone Lattice;
  cluster SkelLatt L -> distributive;
end;

theorem :: LATSTONE:22
  Bottom L = Bottom SkelLatt L & Top L = Top SkelLatt L;

:: LTRS: Proposition 45

registration let L be Stone Lattice;
  cluster SkelLatt L -> Boolean;
end;

begin :: Dense Elements in Lattices

definition let L be lower-bounded Lattice;
  func DenseElements L -> Subset of L equals
:: LATSTONE:def 9
    { a where a is Element of L : a* = Bottom L };
end;

theorem :: LATSTONE:23
  Top L in DenseElements L;

registration let L be Stone Lattice;
  cluster DenseElements L -> non empty;
end;

definition let L be Stone Lattice, a be Element of L;
  attr a is dense means
:: LATSTONE:def 10
    a in DenseElements L;
end;

registration let L be Stone Lattice;
  cluster Top L -> dense;
end;

theorem :: LATSTONE:24
  for L being Stone Lattice, x being Element of L st x in DenseElements L holds
    x* = Bottom L;

registration let L be Stone Lattice;
  cluster DenseElements L -> join-closed meet-closed;
end;

definition let L be Stone Lattice;
  redefine func DenseElements L -> ClosedSubset of L;
end;

:: Set of dense elements equipped with the lattice structure

definition let L be Stone Lattice;
  func DenseLatt L -> Sublattice of L equals
:: LATSTONE:def 11
    latt (L, DenseElements L);
end;

registration let L be Stone Lattice;
  cluster DenseLatt L -> distributive;
end;

:: Meet-decomposition of elements of a lattice in terms
:: of skeletal and dense elements

theorem :: LATSTONE:25
  for L being Stone Lattice, a being Element of L holds
  ex b, c being Element of L st a = b "/\" c & b in Skeleton L &
  c in DenseElements L;

begin :: An Example: Lattice of Natural Divisors

theorem :: LATSTONE:26
  for p being Prime holds NatDivisors p = {1, p};

theorem :: LATSTONE:27
  for p being Prime holds NatDivisors (p * p) = {1, p, p*p};

registration let n be non zero Nat;
  cluster Divisors_Lattice n -> finite;
end;

registration
  cluster complete for Boolean Lattice;
end;

registration let p be Prime;
  cluster Divisors_Lattice (p) -> Boolean;
end;

:: Hence it is pseudocomplemented, and Stone

registration let p be Prime;
  cluster Divisors_Lattice (p * p) -> pseudocomplemented;
end;

theorem :: LATSTONE:28
  for L being Lattice, p being Prime, x being Element of L st
    L = Divisors_Lattice (p * p) & x = p holds x* = Bottom L;

:: The example of a lattice which is Stone but not Boolean

registration let p be Prime;
  cluster Divisors_Lattice (p * p) -> satisfying_Stone_identity;
end;

registration let p be Prime;
  cluster Divisors_Lattice (p * p) -> non Boolean Stone;
end;

registration
  cluster Stone non Boolean for Lattice;
end;

:: Every squarefree number generates Stone lattice as it is Boolean

begin :: Products of Pseudocomplemented Lattices

 reserve L1, L2 for Lattice;
 reserve p1, q1 for Element of L1;
 reserve p2, q2 for Element of L2;

theorem :: LATSTONE:29
  L1 is 01_Lattice & L2 is 01_Lattice implies
    (p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 iff
      [p1,p2] is_a_pseudocomplement_of [q1,q2]);

theorem :: LATSTONE:30
  L1 is 01_Lattice & L2 is 01_Lattice implies (L1 is pseudocomplemented &
  L2 is pseudocomplemented iff [:L1,L2:] is pseudocomplemented);

registration let L1, L2 be pseudocomplemented 01_Lattice;
  cluster [:L1,L2:] -> pseudocomplemented;
end;

theorem :: LATSTONE:31
  L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice
  implies [p1,p2]* = [p1*,p2*];

 reserve L1, L2 for non empty Lattice;

theorem :: LATSTONE:32
  L1 is satisfying_Stone_identity pseudocomplemented 01_Lattice &
  L2 is satisfying_Stone_identity pseudocomplemented 01_Lattice implies
  [:L1,L2:] is satisfying_Stone_identity;

theorem :: LATSTONE:33
  L1 is Stone & L2 is Stone implies [:L1,L2:] is Stone;

registration let L1, L2 be Stone Lattice;
  cluster [:L1,L2:] -> Stone;
end;

begin :: Special Construction: B squared

reserve B for Boolean Lattice;

:: LTRS: Lemma 46 - definition

definition let B be Boolean Lattice;
  func B squared -> Subset of [:B,B:] equals
:: LATSTONE:def 12
    { [a,b] where a, b is Element of B : a [= b };
end;

registration let B be Boolean Lattice;
  cluster B squared -> non empty;
end;

registration let B be Boolean Lattice;
  cluster B squared -> join-closed meet-closed;
end;

definition let B be Boolean Lattice;
  redefine func B squared -> non empty ClosedSubset of [:B,B:];
end;

definition let B be Boolean Lattice;
  func B squared-latt -> Lattice equals
:: LATSTONE:def 13
    latt ([:B,B:], B squared);
end;

theorem :: LATSTONE:34
  the carrier of (B squared-latt) = B squared;

theorem :: LATSTONE:35
  [Bottom B, Bottom B] in the carrier of (B squared-latt);

theorem :: LATSTONE:36
  [Top B, Top B] in the carrier of (B squared-latt);

registration let B be Boolean Lattice;
  cluster B squared-latt -> lower-bounded;
  cluster B squared-latt -> upper-bounded;
end;

theorem :: LATSTONE:37
  Bottom (B squared-latt) = [Bottom B, Bottom B];

theorem :: LATSTONE:38
  Top (B squared-latt) = [Top B, Top B];

registration let B be Boolean Lattice;
  cluster B squared-latt -> pseudocomplemented;
end;

theorem :: LATSTONE:39
  for L being Lattice, x1,x2 being Element of B, x being Element of L st
    L = B squared-latt & x = [x1,x2] holds x* = [x2`,x2`];

registration let B be Boolean Lattice;
  cluster B squared-latt -> satisfying_Stone_identity;
end;

:: LTRS: Lemma 46, p. 425

registration let B be Boolean Lattice;
  cluster B squared-latt -> Stone;
end;

:: Skeleton and dense elements in the lattice B squared

theorem :: LATSTONE:40
  Skeleton (B squared-latt) = the set of all [a,a] where a is Element of B;

theorem :: LATSTONE:41
  DenseElements (B squared-latt) = the set of all [a,Top B]
    where a is Element of B;