:: On the Characterization of Modular and Distributive Lattices
::  by Adam Naumowicz
::
:: Received April 3, 1998
:: Copyright (c) 1998-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, CARD_1, XBOOLE_0, TARSKI, RELAT_2, LATTICE3, ORDERS_2,
      SUBSET_1, LATTICES, EQREL_1, XXREAL_0, WAYBEL_0, YELLOW_1, STRUCT_0,
      CAT_1, LATTICE5, WELLORD1, FUNCT_1, SEQM_3, YELLOW_0, RELAT_1, ORDINAL2,
      MEASURE5, FINSET_1, ORDERS_1, REWRITE1, YELLOW11, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, FUNCT_1, RELSET_1,
      FUNCT_2, ORDINAL1, CARD_1, NUMBERS, ORDERS_1, DOMAIN_1, FINSET_1,
      STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_1,
      LATTICE5, WAYBEL_0;
 constructors DOMAIN_1, XXREAL_0, LATTICE3, ORDERS_3, WAYBEL_1, RELSET_1,
      NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ORDERS_2, LATTICE3,
      YELLOW_0, YELLOW_1, ORDINAL1;
 requirements NUMERALS, REAL, SUBSET, BOOLE;


begin

reserve x for set;

:: Preliminaries

theorem :: YELLOW11:1
  3 = {0,1,2};

theorem :: YELLOW11:2
  2\1={1};

theorem :: YELLOW11:3
  3\1 = {1,2};

theorem :: YELLOW11:4
  3\2 = {2};

begin:: Main part

theorem :: YELLOW11:5
  for L being antisymmetric reflexive with_infima with_suprema
  RelStr for a,b being Element of L holds a"/\"b = b iff a"\/"b = a;

theorem :: YELLOW11:6
  for L being LATTICE for a,b,c being Element of L holds
  (a"/\"b)"\/"(a"/\"c) <= a"/\"(b"\/"c);

theorem :: YELLOW11:7
  for L being LATTICE for a,b,c being Element of L holds
  a"\/"(b"/\"c) <= (a"\/"b)"/\"(a"\/"c);

theorem :: YELLOW11:8
  for L being LATTICE for a,b,c being Element of L holds a <= c
  implies a"\/"(b"/\"c) <= (a"\/"b) "/\"c;

definition
  func N_5 -> RelStr equals
:: YELLOW11:def 1
  InclPoset {0, 3 \ 1, 2, 3 \ 2, 3};
end;

registration
  cluster N_5 -> strict reflexive transitive antisymmetric;
  cluster N_5 -> with_infima with_suprema;
end;

definition
  func M_3 -> RelStr equals
:: YELLOW11:def 2
  InclPoset{ 0, 1, 2 \ 1, 3 \ 2, 3 };
end;

registration
  cluster M_3 -> strict reflexive transitive antisymmetric;
  cluster M_3 -> with_infima with_suprema;
end;

theorem :: YELLOW11:9
  for L being LATTICE holds
  (ex K being full Sublattice of L st N_5,K are_isomorphic) iff
  ex a,b,c,d,e being Element of L st
  a,b,c,d,e are_mutually_distinct &
  a"/\"b = a & a"/\"c = a & c"/\"e = c & d"/\"e = d & b"/\"c = a & b"/\"d = b &
  c"/\"d = a & b"\/"c = e & c"\/"d = e;

theorem :: YELLOW11:10
  for L being LATTICE holds
  (ex K being full Sublattice of L st M_3,K are_isomorphic) iff
  ex a,b,c,d,e being Element of L st a,b,c,d,e are_mutually_distinct &
  a"/\"b = a & a"/\"c = a & a"/\"d = a & b"/\"e = b & c"/\"e = c &
  d"/\"e = d & b"/\"c = a & b"/\"d = a & c"/\"d = a & b"\/"c = e &
  b"\/"d = e & c"\/"d = e;

begin:: Modular lattices

definition
  let L be non empty RelStr;
  attr L is modular means
:: YELLOW11:def 3

  for a,b,c being Element of L st a <= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c;
end;

registration
  cluster distributive -> modular for non empty antisymmetric reflexive
    with_infima RelStr;
end;

theorem :: YELLOW11:11
  for L being LATTICE holds
  L is modular iff not ex K being full Sublattice of L st N_5,K are_isomorphic;

theorem :: YELLOW11:12
  for L being LATTICE st L is modular holds L is distributive iff not ex
  K being full Sublattice of L st M_3,K are_isomorphic;

begin:: Intervals of a lattice

definition
  let L be non empty RelStr;
  let a,b be Element of L;
  func [#a,b#] -> Subset of L means
:: YELLOW11:def 4

  for c being Element of L holds c in it iff a <= c & c <= b;
end;

definition
  let L be non empty RelStr;
  let IT be Subset of L;
  attr IT is interval means
:: YELLOW11:def 5

  ex a,b being Element of L st IT = [#a,b#];
end;

registration
  let L be non empty reflexive transitive RelStr;
  cluster non empty interval -> directed for (Subset of L);
  cluster non empty interval -> filtered for (Subset of L);
end;

registration
  let L be non empty RelStr;
  let a,b be Element of L;
  cluster [#a,b#] -> interval;
end;

theorem :: YELLOW11:13
  for L being non empty reflexive transitive RelStr, a,b being Element
  of L holds [#a,b#] = uparrow a /\ downarrow b;

registration
  let L be with_infima Poset;
  let a,b be Element of L;
  cluster subrelstr[#a,b#] -> meet-inheriting;
end;

registration
  let L be with_suprema Poset;
  let a,b be Element of L;
  cluster subrelstr[#a,b#] -> join-inheriting;
end;

theorem :: YELLOW11:14
  for L being LATTICE, a,b being Element of L holds L is modular implies
  subrelstr[#b,a"\/"b#],subrelstr[#a"/\" b,a#] are_isomorphic;

registration
  cluster finite non empty for LATTICE;
end;

registration
  cluster finite -> lower-bounded for Semilattice;
end;

registration
  cluster finite -> complete for LATTICE;
end;