:: Noetherian Lattices
::  by Christoph Schwarzweller
::
:: Received June 9, 1999
:: Copyright (c) 1999-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 FINSET_1, LATTICES, LATTICE3, XBOOLE_0, STRUCT_0, ZFMISC_1,
      SUBSET_1, XXREAL_0, NUMBERS, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, FUNCT_1,
      TARSKI, ORDERS_2, FILTER_1, EQREL_1, PBOOLE, REWRITE1, WELLORD1,
      WAYBEL_6, RELAT_2, ZF_LANG, BINOP_1, LATTICE6, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
      RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, BINOP_1, FINSET_1, WELLORD1, WAYBEL_6,
      STRUCT_0, LATTICES, LATTICE3, ORDERS_2, FINSEQ_1, WELLFND1, YELLOW_0,
      LATTICE2;
 constructors WELLORD1, BINOP_1, REAL_1, REALSET2, LATTICE2, WAYBEL_0,
      WAYBEL_6, WELLFND1, RELSET_1, LATTICE3;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, INT_1, FINSEQ_1,
      FINSEQ_6, STRUCT_0, LATTICES, ORDERS_2, LATTICE2, LATTICE3, WAYBEL_0,
      KNASTER, YELLOW_1, ORDINAL1, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

registration
  cluster finite for Lattice;
end;

registration
  cluster finite -> complete for Lattice;
end;

definition
  let L be Lattice;
  let D be Subset of L;
  func D% -> Subset of LattPOSet L equals
:: LATTICE6:def 1
  {d% where d is Element of L : d in D
  };
end;

definition
  let L be Lattice;
  let D be Subset of LattPOSet L;
  func %D -> Subset of L equals
:: LATTICE6:def 2
  {%d where d is Element of LattPOSet L : d in D
  };
end;

registration
  let L be finite Lattice;
  cluster LattPOSet L -> well_founded;
end;

definition
  let L be Lattice;
  attr L is noetherian means
:: LATTICE6:def 3

  LattPOSet L is well_founded;
  attr L is co-noetherian means
:: LATTICE6:def 4

  (LattPOSet L)~ is well_founded;
end;

registration
  cluster noetherian upper-bounded lower-bounded complete for Lattice;
end;

registration
  cluster co-noetherian upper-bounded lower-bounded complete for Lattice;
end;

theorem :: LATTICE6:1
  for L being Lattice holds L is noetherian iff L.: is co-noetherian;

registration
  cluster finite -> noetherian for Lattice;
  cluster finite -> co-noetherian for Lattice;
end;

definition
  let L be Lattice;
  let a,b be Element of L;
  pred a is-upper-neighbour-of b means
:: LATTICE6:def 5

  a <> b & b [= a & for c being
  Element of L holds b [= c & c [= a implies (c = a or c = b);
end;

notation
  let L be Lattice;
  let a,b be Element of L;
  synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;
end;

theorem :: LATTICE6:2
  for L being Lattice for a being Element of L for b,c being
  Element of L st b <> c holds ( b is-upper-neighbour-of a & c
is-upper-neighbour-of a implies a = c "/\" b) & ( b is-lower-neighbour-of a & c
  is-lower-neighbour-of a implies a = c "\/" b);

theorem :: LATTICE6:3
  for L being noetherian Lattice for a being Element of L for d
being Element of L st a [= d & a <> d holds ex c being Element of L st c [= d &
  c is-upper-neighbour-of a;

theorem :: LATTICE6:4
  for L being co-noetherian Lattice for a being Element of L for d
being Element of L st d [= a & a <> d holds ex c being Element of L st d [= c &
  c is-lower-neighbour-of a;

theorem :: LATTICE6:5
  for L being upper-bounded Lattice holds not(ex b being Element of
  L st b is-upper-neighbour-of Top L);

theorem :: LATTICE6:6
  for L being noetherian upper-bounded Lattice for a being Element
of L holds a = Top L iff not(ex b being Element of L st b is-upper-neighbour-of
  a);

theorem :: LATTICE6:7
  for L being lower-bounded Lattice holds not(ex b being Element of
  L st b is-lower-neighbour-of Bottom L);

theorem :: LATTICE6:8
  for L being co-noetherian lower-bounded Lattice for a being
  Element of L holds a = Bottom L iff not(ex b being Element of L st b
  is-lower-neighbour-of a);

definition
  let L be complete Lattice;
  let a be Element of L;
  func a*' -> Element of L equals
:: LATTICE6:def 6
  "/\"({d where d is Element of L : a [= d & d
  <> a},L);
  func *'a -> Element of L equals
:: LATTICE6:def 7
  "\/"({d where d is Element of L : d [= a & d
  <> a},L);
end;

definition
  let L be complete Lattice;
  let a be Element of L;
  attr a is completely-meet-irreducible means
:: LATTICE6:def 8

  a*' <> a;
  attr a is completely-join-irreducible means
:: LATTICE6:def 9

  *'a <> a;
end;

theorem :: LATTICE6:9
  for L being complete Lattice for a being Element of L holds a [=
  a*' & *'a [= a;

theorem :: LATTICE6:10
  for L being complete Lattice holds Top L*' = Top L & (Top L)% is
  meet-irreducible;

theorem :: LATTICE6:11
  for L being complete Lattice holds *'Bottom L = Bottom L & (Bottom L)%
  is join-irreducible;

theorem :: LATTICE6:12
  for L being complete Lattice for a being Element of L st a is
  completely-meet-irreducible holds a*' is-upper-neighbour-of a & for c being
  Element of L holds c is-upper-neighbour-of a implies c = a*';

theorem :: LATTICE6:13
  for L being complete Lattice for a being Element of L st a is
  completely-join-irreducible holds *'a is-lower-neighbour-of a & for c being
  Element of L holds c is-lower-neighbour-of a implies c = *'a;

theorem :: LATTICE6:14
  for L being noetherian complete Lattice for a being Element of L
  holds a is completely-meet-irreducible iff ex b being Element of L st b
  is-upper-neighbour-of a & for c being Element of L holds c
  is-upper-neighbour-of a implies c = b;

theorem :: LATTICE6:15
  for L being co-noetherian complete Lattice for a being Element
  of L holds a is completely-join-irreducible iff ex b being Element of L st b
  is-lower-neighbour-of a & for c being Element of L holds c
  is-lower-neighbour-of a implies c = b;

theorem :: LATTICE6:16
  for L being complete Lattice for a being Element of L holds a is
  completely-meet-irreducible implies a% is meet-irreducible;

theorem :: LATTICE6:17
  for L being complete noetherian Lattice for a being Element of L
st a <> Top L holds a is completely-meet-irreducible iff a% is meet-irreducible
;

theorem :: LATTICE6:18
  for L being complete Lattice for a being Element of L holds a is
  completely-join-irreducible implies a% is join-irreducible;

theorem :: LATTICE6:19
  for L being complete co-noetherian Lattice for a being Element
  of L st a <> Bottom L holds a is completely-join-irreducible iff a% is
  join-irreducible;

theorem :: LATTICE6:20
  for L being finite Lattice for a being Element of L st a <> Bottom L &
a <> Top L holds (a is completely-meet-irreducible iff a% is meet-irreducible)
  & (a is completely-join-irreducible iff a% is join-irreducible);

definition
  let L be Lattice;
  let a be Element of L;
  attr a is atomic means
:: LATTICE6:def 10

  a is-upper-neighbour-of Bottom L;
  attr a is co-atomic means
:: LATTICE6:def 11

  a is-lower-neighbour-of Top L;
end;

theorem :: LATTICE6:21
  for L being complete Lattice for a being Element of L st a is atomic
  holds a is completely-join-irreducible;

theorem :: LATTICE6:22
  for L being complete Lattice for a being Element of L st a is
  co-atomic holds a is completely-meet-irreducible;

definition
  let L be Lattice;
  attr L is atomic means
:: LATTICE6:def 12

  for a being Element of L holds ex X being
  Subset of L st (for x being Element of L st x in X holds x is atomic) & a =
  "\/"(X,L);
end;

registration
  cluster strict 1-element for Lattice;
end;

registration
  cluster atomic complete for Lattice;
end;

definition
  let L be complete Lattice;
  let D be Subset of L;
  attr D is supremum-dense means
:: LATTICE6:def 13

  for a being Element of L holds ex D9 being Subset of D st a = "\/"(D9,L);
  attr D is infimum-dense means
:: LATTICE6:def 14

  for a being Element of L holds ex D9 being Subset of D st a = "/\"(D9,L);
end;

theorem :: LATTICE6:23
  for L being complete Lattice for D being Subset of L holds D is
  supremum-dense iff for a being Element of L holds a = "\/"({d where d is
  Element of L: d in D & d [= a},L);

theorem :: LATTICE6:24
  for L being complete Lattice for D being Subset of L holds D is
infimum-dense iff for a being Element of L holds a = "/\"({d where d is Element
  of L : d in D & a [= d},L);

theorem :: LATTICE6:25
  for L being complete Lattice for D being Subset of L holds D is
  infimum-dense iff D% is order-generating;

definition
  let L be complete Lattice;
  func MIRRS(L) -> Subset of L equals
:: LATTICE6:def 15
  {a where a is Element of L : a is
  completely-meet-irreducible};
  func JIRRS(L) -> Subset of L equals
:: LATTICE6:def 16
  {a where a is Element of L : a is
  completely-join-irreducible };
end;

theorem :: LATTICE6:26
  for L being complete Lattice for D being Subset of L st D is
  supremum-dense holds JIRRS(L) c= D;

theorem :: LATTICE6:27
  for L being complete Lattice for D being Subset of L st D is
  infimum-dense holds MIRRS(L) c= D;

registration
  let L be co-noetherian complete Lattice;
  cluster MIRRS(L) -> infimum-dense;
end;

registration
  let L be noetherian complete Lattice;
  cluster JIRRS(L) -> supremum-dense;
end;