The abstract of the Mizar article:

Noetherian Lattices

by

Christoph Schwarzweller

Received June 9, 1999

MML identifier: LATTICE6

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSET_1, LATTICES, LATTICE3, BOOLE, FINSEQ_1, RELAT_1, FUNCT_1,
      ORDERS_1, FILTER_1, RELAT_2, BHSP_3, WELLORD1, ARYTM_3, WAYBEL_6,
      ZF_LANG, REALSET1, BINOP_1, TARSKI, LATTICE6;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1,
      NAT_1, STRUCT_0, BINOP_1, LATTICES, LATTICE3, FINSET_1, WELLORD1,
      WAYBEL_6, GROUP_1, ORDERS_1, FINSEQ_1, WELLFND1, YELLOW_0, LATTICE2,
      REALSET1;
 constructors LATTICE2, WAYBEL_1, WAYBEL_6, NAT_1, GROUP_1, WELLFND1, WELLORD1,
      BINOP_1, REALSET1, MEMBERED;
 clusters SUBSET_1, STRUCT_0, LATTICE2, LATTICE3, YELLOW_1, FINSET_1, ORDERS_1,
      INT_1, FINSEQ_1, FINSEQ_6, WAYBEL_0, KNASTER, LATTICES;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

definition
cluster finite Lattice;
end;

definition
cluster finite -> complete 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;

definition 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;

definition
cluster noetherian upper-bounded lower-bounded complete Lattice;
end;

definition
cluster co-noetherian upper-bounded lower-bounded complete Lattice;
end;

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

definition
cluster finite -> noetherian Lattice;
cluster finite -> co-noetherian 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);
synonym b is-lower-neighbour-of a;
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;

definition
  cluster strict non empty trivial Lattice;
end;

definition
cluster atomic complete 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 D' being Subset of D st a = "\/"(D',L);
attr D is infimum-dense means
:: LATTICE6:def 14
 for a being Element of L holds
 ex D' being Subset of D st a = "/\"(D',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;

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

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