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