:: Meet-continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received October 10, 1996
:: Copyright (c) 1996-2016 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 XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, RELAT_2, LATTICE3,
ORDERS_2, XXREAL_0, TREES_2, WAYBEL_0, YELLOW_0, LATTICES, EQREL_1,
ORDINAL2, ZFMISC_1, TARSKI, STRUCT_0, MCART_1, SEQM_3, REWRITE1,
FINSET_1, WELLORD1, CAT_1, YELLOW_2, FINSUB_1, WELLORD2, YELLOW_1,
CARD_FIL, LATTICE2, WAYBEL_1, WAYBEL_2, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1,
RELSET_1, TOLER_1, FINSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1,
ORDERS_1, STRUCT_0, ORDERS_2, ORDERS_3, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4;
constructors DOMAIN_1, FINSUB_1, TOLER_1, ORDERS_3, WAYBEL_1, YELLOW_3,
YELLOW_4, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
FINSUB_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
WAYBEL_1, YELLOW_3, YELLOW_4, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE, NUMERALS;
begin :: Preliminaries
registration
let X, Y be non empty set, f be Function of X, Y, Z be non empty Subset of X;
cluster f.:Z -> non empty;
end;
registration
cluster reflexive connected -> with_infima with_suprema for
non empty RelStr;
end;
registration
let C be Chain;
cluster [#]C -> directed;
end;
theorem :: WAYBEL_2:1
for L being up-complete Semilattice for D being non empty
directed Subset of L, x being Element of L holds ex_sup_of {x} "/\" D,L;
theorem :: WAYBEL_2:2
for L being up-complete sup-Semilattice for D being non empty directed
Subset of L, x being Element of L holds ex_sup_of {x} "\/" D,L;
theorem :: WAYBEL_2:3
for L being up-complete sup-Semilattice for A, B being non empty
directed Subset of L holds A is_<=_than sup (A "\/" B);
theorem :: WAYBEL_2:4
for L being up-complete sup-Semilattice for A, B being non empty
directed Subset of L holds sup (A "\/" B) = sup A "\/" sup B;
theorem :: WAYBEL_2:5
for L being up-complete Semilattice for D being non empty
directed Subset of [:L,L:] holds { sup ({x} "/\" proj2 D) where x is Element of
L: x in proj1 D } = { sup X where X is non empty directed Subset of L: ex x
being Element of L st X = {x} "/\" proj2 D & x in proj1 D };
theorem :: WAYBEL_2:6
for L being Semilattice, D being non empty directed Subset of [:L
,L:] holds union {X where X is non empty directed Subset of L: ex x being
Element of L st X = {x} "/\" proj2 D & x in proj1 D} = proj1 D "/\" proj2 D;
theorem :: WAYBEL_2:7
for L being up-complete Semilattice for D being non empty
directed Subset of [:L,L:] holds ex_sup_of union {X where X is non empty
directed Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in
proj1 D},L;
theorem :: WAYBEL_2:8
for L being up-complete Semilattice for D being non empty
directed Subset of [:L,L:] holds ex_sup_of {sup X where X is non empty directed
Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L;
theorem :: WAYBEL_2:9
for L being up-complete Semilattice for D being non empty
directed Subset of [:L,L:] holds "\/" ({ sup X where X is non empty directed
Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D },L
) <= "\/" (union {X where X is non empty directed Subset of L: ex x being
Element of L st X = {x} "/\" proj2 D & x in proj1 D},L);
theorem :: WAYBEL_2:10
for L being up-complete Semilattice for D being non empty
directed Subset of [:L,L:] holds "\/" ({ sup X where X is non empty directed
Subset of L: ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L)
= "\/" (union {X where X is non empty directed Subset of L: ex x being Element
of L st X = {x} "/\" proj2 D & x in proj1 D},L);
registration
let S, T be up-complete non empty reflexive RelStr;
cluster [:S,T:] -> up-complete;
end;
theorem :: WAYBEL_2:11
for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is
up-complete holds S is up-complete & T is up-complete;
theorem :: WAYBEL_2:12
for L being up-complete antisymmetric non empty reflexive
RelStr for D being non empty directed Subset of [:L,L:] holds sup D = [sup
proj1 D,sup proj2 D];
theorem :: WAYBEL_2:13
for S1, S2 being RelStr, D being Subset of S1 for f being
Function of S1,S2 st f is monotone holds f.:(downarrow D) c= downarrow (f.:D)
;
theorem :: WAYBEL_2:14
for S1, S2 being RelStr, D being Subset of S1 for f being
Function of S1,S2 st f is monotone holds f.:(uparrow D) c= uparrow (f.:D);
registration
cluster -> distributive complemented for 1-element reflexive RelStr;
end;
registration
cluster strict 1-element for LATTICE;
end;
theorem :: WAYBEL_2:15
for H being distributive complete LATTICE for a being Element of
H, X being finite Subset of H holds sup ({a} "/\" X) = a "/\" sup X;
theorem :: WAYBEL_2:16
for H being distributive complete LATTICE for a being Element of H, X
being finite Subset of H holds inf ({a} "\/" X) = a "\/" inf X;
theorem :: WAYBEL_2:17
for H being complete distributive LATTICE, a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X;
begin :: The Properties of Nets
scheme :: WAYBEL_2:sch 1
ExNet { L() -> non empty RelStr, N() -> prenet of L(), F(set) -> Element of
L()} : ex M being prenet of L() st the RelStr of M = the RelStr of N() & for i
being Element of M holds (the mapping of M).i = F((the mapping of N()).i);
theorem :: WAYBEL_2:18
for L being non empty RelStr for N being prenet of L st N is
eventually-directed holds rng netmap (N,L) is directed;
theorem :: WAYBEL_2:19
for L being non empty reflexive RelStr, D being non empty
directed Subset of L for n being Function of D, the carrier of L holds NetStr
(#D,(the InternalRel of L)|_2 D,n#) is prenet of L;
theorem :: WAYBEL_2:20
for L being non empty reflexive RelStr, D being non empty
directed Subset of L for n being Function of D, the carrier of L, N being
prenet of L st n = id D & N = NetStr (#D,(the InternalRel of L)|_2 D,n#) holds
N is eventually-directed;
definition
let L be non empty RelStr, N be NetStr over L;
func sup N -> Element of L equals
:: WAYBEL_2:def 1
Sup the mapping of N;
end;
definition
let L be non empty RelStr, J be set, f be Function of J,the carrier of L;
func FinSups f -> prenet of L means
:: WAYBEL_2:def 2
ex g being Function of Fin J, the
carrier of L st for x being Element of Fin J holds g.x = sup (f.:x) & it =
NetStr (# Fin J, RelIncl Fin J, g #);
end;
theorem :: WAYBEL_2:21
for L being non empty RelStr, J, x being set for f being Function of J
,the carrier of L holds x is Element of FinSups f iff x is Element of Fin J;
registration
let L be complete antisymmetric non empty reflexive RelStr, J be set, f be
Function of J,the carrier of L;
cluster FinSups f -> monotone;
end;
definition
let L be non empty RelStr, x be Element of L, N be non empty NetStr over L;
func x "/\" N -> strict NetStr over L means
:: WAYBEL_2:def 3
the RelStr of it = the
RelStr of N & for i being Element of it ex y being Element of L st y = (the
mapping of N).i & (the mapping of it).i = x "/\" y;
end;
theorem :: WAYBEL_2:22
for L being non empty RelStr, N being non empty NetStr over L
for x being Element of L, y being set holds y is Element of N iff y is Element
of x "/\" N;
registration
let L be non empty RelStr, x be Element of L, N be non empty NetStr over L;
cluster x "/\" N -> non empty;
end;
registration
let L be non empty RelStr, x be Element of L, N be prenet of L;
cluster x "/\" N -> directed;
end;
theorem :: WAYBEL_2:23
for L being non empty RelStr, x being Element of L for F being
non empty NetStr over L holds rng (the mapping of x "/\" F) = {x} "/\" rng the
mapping of F;
theorem :: WAYBEL_2:24
for L being non empty RelStr, J being set for f being Function
of J,the carrier of L st for x being set holds ex_sup_of f.:x,L holds rng
netmap(FinSups f,L) c= finsups rng f;
theorem :: WAYBEL_2:25
for L being non empty reflexive antisymmetric RelStr, J being
set for f being Function of J,the carrier of L holds rng f c= rng netmap (
FinSups f,L);
theorem :: WAYBEL_2:26
for L being non empty reflexive antisymmetric RelStr, J being
set for f being Function of J,the carrier of L st ex_sup_of rng f,L & ex_sup_of
rng netmap (FinSups f,L),L & for x being Element of Fin J holds ex_sup_of f.:x,
L holds Sup f = sup FinSups f;
theorem :: WAYBEL_2:27
for L being with_infima antisymmetric transitive RelStr, N being
prenet of L for x being Element of L st N is eventually-directed holds x "/\" N
is eventually-directed;
theorem :: WAYBEL_2:28
for L being up-complete Semilattice st for x being Element of L,
E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E
) holds for D being non empty directed Subset of L, x being Element of L holds
x "/\" sup D = sup ({x} "/\" D);
theorem :: WAYBEL_2:29
for L being with_suprema Poset st for X being directed Subset of L, x
being Element of L holds x "/\" sup X = sup ({x} "/\" X) holds for X being
Subset of L, x being Element of L st ex_sup_of X,L holds x "/\" sup X = sup ({x
} "/\" finsups X);
theorem :: WAYBEL_2:30
for L being up-complete LATTICE st for X being Subset of L, x being
Element of L holds x "/\" sup X = sup ({x} "/\" finsups X) holds for X being
non empty directed Subset of L, x being Element of L holds x "/\" sup X = sup (
{x} "/\" X);
begin :: On the inf and sup operation
definition
let L be non empty RelStr;
func inf_op L -> Function of [:L,L:], L means
:: WAYBEL_2:def 4
for x, y being Element of L holds it.(x,y) = x "/\" y;
end;
theorem :: WAYBEL_2:31
for L being non empty RelStr, x being Element of [:L,L:] holds (
inf_op L).x = x`1 "/\" x`2;
registration
let L be with_infima transitive antisymmetric RelStr;
cluster inf_op L -> monotone;
end;
theorem :: WAYBEL_2:32
for S being non empty RelStr, D1, D2 being Subset of S holds (
inf_op S).:[:D1,D2:] = D1 "/\" D2;
theorem :: WAYBEL_2:33
for L being up-complete Semilattice for D being non empty
directed Subset of [:L,L:] holds sup ((inf_op L).:D) = sup (proj1 D "/\" proj2
D);
definition
let L be non empty RelStr;
func sup_op L -> Function of [:L,L:], L means
:: WAYBEL_2:def 5
for x, y being Element of L holds it.(x,y) = x "\/" y;
end;
theorem :: WAYBEL_2:34
for L being non empty RelStr, x being Element of [:L,L:] holds (
sup_op L).x = x`1 "\/" x`2;
registration
let L be with_suprema transitive antisymmetric RelStr;
cluster sup_op L -> monotone;
end;
theorem :: WAYBEL_2:35
for S being non empty RelStr, D1, D2 being Subset of S holds (
sup_op S).:[:D1,D2:] = D1 "\/" D2;
theorem :: WAYBEL_2:36
for L being complete non empty Poset for D being non empty filtered
Subset of [:L,L:] holds inf ((sup_op L).:D) = inf (proj1 D "\/" proj2 D);
begin :: Meet-continuous lattices
:: Def 4.1, s.30
definition
let R be non empty reflexive RelStr;
attr R is satisfying_MC means
:: WAYBEL_2:def 6
for x being Element of R, D being non
empty directed Subset of R holds x "/\" sup D = sup ({x} "/\" D);
end;
definition
let R be non empty reflexive RelStr;
attr R is meet-continuous means
:: WAYBEL_2:def 7
R is up-complete satisfying_MC;
end;
registration
cluster -> satisfying_MC for 1-element reflexive RelStr;
end;
registration
cluster meet-continuous -> up-complete satisfying_MC for non empty reflexive
RelStr;
cluster up-complete satisfying_MC -> meet-continuous for non empty reflexive
RelStr;
end;
theorem :: WAYBEL_2:37
for S being non empty reflexive RelStr st for X being Subset of
S, x being Element of S holds x "/\" sup X = "\/"({x"/\"y where y is Element of
S: y in X},S) holds S is satisfying_MC;
:: Th 4.2, s.30, 1 => 2
theorem :: WAYBEL_2:38
for L being up-complete Semilattice st SupMap L is
meet-preserving holds for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2)
= sup (I1 "/\" I2);
registration
let L be up-complete sup-Semilattice;
cluster SupMap L -> join-preserving;
end;
:: Th 4.2, s.30, 2 => 1
theorem :: WAYBEL_2:39
for L being up-complete Semilattice st for I1, I2 being Ideal of
L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) holds SupMap L is
meet-preserving;
:: Th 4.2, s.30, 2 => 3
theorem :: WAYBEL_2:40
for L being up-complete Semilattice st for I1, I2 being Ideal of
L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) holds for D1, D2 be directed
non empty Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2);
:: Th 4.2, s.30, 4 => 7
theorem :: WAYBEL_2:41
for L being non empty reflexive RelStr st L is satisfying_MC
holds for x being Element of L, N being non empty prenet of L st N is
eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L));
:: Th 4.2, s.30, 7 => 4
theorem :: WAYBEL_2:42
for L being non empty reflexive RelStr st for x being Element of
L, N being prenet of L st N is eventually-directed holds x "/\" sup N = sup ({x
} "/\" rng netmap (N,L)) holds L is satisfying_MC;
:: Th 4.2, s.30, 6 => 3
theorem :: WAYBEL_2:43
for L being up-complete antisymmetric non empty reflexive
RelStr st inf_op L is directed-sups-preserving holds for D1, D2 being non
empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2);
:: Th 4.2, s.30, 3 => 4
theorem :: WAYBEL_2:44
for L being non empty reflexive antisymmetric RelStr st for D1,
D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1
"/\" D2) holds L is satisfying_MC;
:: Th 4.2, s.30, MC => 5
theorem :: WAYBEL_2:45
for L being satisfying_MC with_infima antisymmetric non empty
reflexive RelStr holds for x being Element of L, D being non empty directed
Subset of L st x <= sup D holds x = sup ({x} "/\" D);
:: Th 4.2, s.30, 5 => 6
theorem :: WAYBEL_2:46
for L being up-complete Semilattice st for x being Element of L,
E being non empty directed Subset of L st x <= sup E holds x <= sup ({x} "/\" E
) holds inf_op L is directed-sups-preserving;
:: Th 4.2, s.30, 7 => 8
theorem :: WAYBEL_2:47
for L being complete antisymmetric non empty reflexive RelStr
st for x being Element of L, N being prenet of L st N is eventually-directed
holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds for x being Element
of L, J being set, f being Function of J,the carrier of L holds x "/\" Sup f =
sup(x "/\" FinSups f);
:: Th 4.2, s.30, 8 => 7
theorem :: WAYBEL_2:48
for L being complete Semilattice st for x being Element of L, J
being set, f being Function of J,the carrier of L holds x "/\" Sup f = sup (x
"/\" FinSups f) holds for x being Element of L, N being prenet of L st N is
eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L));
:: Th 4.2, s.30, 4 <=> 1
theorem :: WAYBEL_2:49
for L being up-complete LATTICE holds L is meet-continuous iff
SupMap L is meet-preserving join-preserving;
registration
let L be meet-continuous LATTICE;
cluster SupMap L -> meet-preserving join-preserving;
end;
:: Th 4.2, s.30, 4 <=> 2
theorem :: WAYBEL_2:50
for L being up-complete LATTICE holds L is meet-continuous iff
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2);
:: Th 4.2, s.30, 4 <=> 3
theorem :: WAYBEL_2:51
for L being up-complete LATTICE holds L is meet-continuous iff
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) =
sup (D1 "/\" D2);
:: Th 4.2, s.30, 4 <=> 5
theorem :: WAYBEL_2:52
for L being up-complete LATTICE holds L is meet-continuous iff for x
being Element of L, D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D);
:: Th 4.2, s.30, 4 <=> 6
theorem :: WAYBEL_2:53
for L being up-complete Semilattice holds L is meet-continuous
iff inf_op L is directed-sups-preserving;
registration
let L be meet-continuous Semilattice;
cluster inf_op L -> directed-sups-preserving;
end;
:: Th 4.2, s.30, 4 <=> 7
theorem :: WAYBEL_2:54
for L being up-complete Semilattice holds L is meet-continuous
iff for x being Element of L, N being non empty prenet of L st N is
eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L));
:: Th 4.2, s.30, 4 <=> 8
theorem :: WAYBEL_2:55
for L being complete Semilattice holds L is meet-continuous iff for x
being Element of L, J being set for f being Function of J,the carrier of L
holds x "/\" Sup f = sup(x "/\" FinSups f);
registration
let L be meet-continuous Semilattice, x be Element of L;
cluster x "/\" -> directed-sups-preserving;
end;
:: Remark 4.3 s.31
theorem :: WAYBEL_2:56
for H being complete non empty Poset holds H is Heyting iff H
is meet-continuous distributive;
registration
cluster complete Heyting -> meet-continuous distributive for
non empty Poset;
cluster complete meet-continuous distributive -> Heyting for
non empty Poset;
end;