:: Properties of Relational Structures, Posets, Lattices and Maps
:: by Mariusz \.Zynel and Czes{\l}aw Byli\'nski
::
:: Received September 20, 1996
:: Copyright (c) 1996-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 XBOOLE_0, ORDERS_2, SUBSET_1, TARSKI, WAYBEL_0, LATTICE3,
XXREAL_0, RELAT_2, YELLOW_0, EQREL_1, LATTICES, RELAT_1, WELLORD1, CAT_1,
STRUCT_0, FUNCT_1, GROUP_6, SEQM_3, ORDINAL2, BINOP_1, REWRITE1,
SETFAM_1, CARD_FIL, YELLOW_1, ZFMISC_1, WELLORD2, YELLOW_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, SETFAM_1, LATTICE3, WELLORD1, DOMAIN_1, ORDERS_1,
STRUCT_0, ORDERS_2, QUANTAL1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0;
constructors SETFAM_1, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_0,
YELLOW_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_1;
requirements SUBSET, BOOLE;
begin :: Basic Facts
reserve x, X, Y for set;
theorem :: YELLOW_2:1
for L being non empty RelStr for x being Element of L for X being
Subset of L holds X c= downarrow x iff X is_<=_than x;
theorem :: YELLOW_2:2
for L being non empty RelStr for x being Element of L for X being
Subset of L holds X c= uparrow x iff x is_<=_than X;
theorem :: YELLOW_2:3
for L being antisymmetric transitive with_suprema RelStr for X, Y
being set st ex_sup_of X,L & ex_sup_of Y,L holds ex_sup_of (X \/ Y),L & "\/"(X
\/ Y, L) = "\/"(X, L) "\/" "\/"(Y, L);
theorem :: YELLOW_2:4
for L being antisymmetric transitive with_infima RelStr for X, Y being
set st ex_inf_of X,L & ex_inf_of Y,L holds ex_inf_of (X \/ Y),L & "/\"(X \/ Y,
L) = "/\"(X, L) "/\" "/\"(Y, L);
begin :: Relational Substructures
theorem :: YELLOW_2:5
for R being Relation for X, Y being set holds X c= Y implies R
|_2 X c= R |_2 Y;
theorem :: YELLOW_2:6
for L being RelStr for S, T being full SubRelStr of L st the carrier
of S c= the carrier of T holds the InternalRel of S c= the InternalRel of T;
theorem :: YELLOW_2:7
for L being non empty RelStr for S being non empty SubRelStr of L
holds (X is directed Subset of S implies X is directed Subset of L) & (X is
filtered Subset of S implies X is filtered Subset of L);
theorem :: YELLOW_2:8
for L being non empty RelStr for S, T being non empty full SubRelStr
of L st the carrier of S c= the carrier of T for X being Subset of S holds X is
Subset of T & for Y being Subset of T st X = Y holds (X is filtered implies Y
is filtered) & (X is directed implies Y is directed);
begin :: Maps
definition
let J be set, L be RelStr;
let f, g be Function of J, the carrier of L;
pred f <= g means
:: YELLOW_2:def 1
for j being set st j in J ex a, b being Element of
L st a = f.j & b = g.j & a <= b;
end;
notation
let J be set, L be RelStr;
let f, g be Function of J, the carrier of L;
synonym g >= f for f <= g;
end;
theorem :: YELLOW_2:9
for L, M being non empty RelStr, f,g being Function of L, M holds f <=
g iff for x being Element of L holds f.x <= g.x;
begin :: The Image of a Map
definition
let L, M be non empty RelStr;
let f be Function of L, M;
func Image f -> strict full SubRelStr of M equals
:: YELLOW_2:def 2
subrelstr rng f;
end;
theorem :: YELLOW_2:10
for L, M being non empty RelStr for f being Function of L, M for y
being Element of Image f ex x being Element of L st f.x = y;
registration
let L be non empty RelStr;
let X be non empty Subset of L;
cluster subrelstr X -> non empty;
end;
registration
let L, M be non empty RelStr;
let f be Function of L, M;
cluster Image f -> non empty;
end;
begin :: Monotone Maps
theorem :: YELLOW_2:11
for L being non empty RelStr holds id L is monotone;
theorem :: YELLOW_2:12
for L, M, N being non empty RelStr for f being Function of L, M, g
being Function of M, N holds f is monotone & g is monotone implies g*f is
monotone;
theorem :: YELLOW_2:13
for L, M being non empty RelStr for f being Function of L, M for X
being Subset of L, x being Element of L holds f is monotone & x is_<=_than X
implies f.x is_<=_than f.:X;
theorem :: YELLOW_2:14
for L, M being non empty RelStr for f being Function of L, M for X
being Subset of L, x being Element of L holds f is monotone & X is_<=_than x
implies f.:X is_<=_than f.x;
theorem :: YELLOW_2:15
for S, T being non empty RelStr for f being Function of S, T for X
being directed Subset of S holds f is monotone implies f.:X is directed;
theorem :: YELLOW_2:16
for L being with_suprema Poset for f being Function of L, L
holds f is directed-sups-preserving implies f is monotone;
theorem :: YELLOW_2:17
for L being with_infima Poset for f being Function of L, L holds f is
filtered-infs-preserving implies f is monotone;
begin :: Idempotent Maps
theorem :: YELLOW_2:18
for S being non empty 1-sorted for f being Function of S, S holds f is
idempotent implies for x being Element of S holds f.(f.x) = f.x;
theorem :: YELLOW_2:19
for S being non empty 1-sorted for f being Function of S, S
holds f is idempotent implies rng f = {x where x is Element of S: x = f.x};
theorem :: YELLOW_2:20
for S being non empty 1-sorted for f being Function of S, S st f
is idempotent holds X c= rng f implies f.:X = X;
theorem :: YELLOW_2:21
for L being non empty RelStr holds id L is idempotent;
begin :: Complete Lattices (CCL Chapter 0, Section 2, pp. 8 -- 9)
reserve L for complete LATTICE,
a for Element of L;
theorem :: YELLOW_2:22
a in X implies a <= "\/"(X, L) & "/\"(X, L) <= a;
theorem :: YELLOW_2:23
for L being non empty RelStr holds (for X holds ex_sup_of X,L)
iff (for Y holds ex_inf_of Y,L);
theorem :: YELLOW_2:24 ::Proposition 2.2 (i) (variant 1) cf YELLOW_0
for L being non empty RelStr holds (for X holds ex_sup_of X,L)
implies L is complete;
theorem :: YELLOW_2:25 ::Proposition 2.2 (i) (variant 2) cf variant 3
for L being non empty RelStr holds (for X holds ex_inf_of X,L)
implies L is complete;
theorem :: YELLOW_2:26
for L being non empty RelStr holds (for A being Subset of L
holds ex_inf_of A, L) implies for X holds ex_inf_of X,L & "/\"(X, L) = "/\"(X
/\ the carrier of L, L);
theorem :: YELLOW_2:27
for L being non empty RelStr holds (for A being Subset of L holds
ex_sup_of A, L) implies for X holds ex_sup_of X,L & "\/"(X, L) = "\/"(X /\ the
carrier of L, L);
theorem :: YELLOW_2:28 ::Proposition 2.2 (i) (variant 3)
for L being non empty RelStr holds (for A being Subset of L
holds ex_inf_of A,L) implies L is complete;
registration
cluster up-complete /\-complete upper-bounded -> complete for
non empty Poset;
end;
theorem :: YELLOW_2:29 :: Theorem 2.3 (The Fixed-Point Theorem)
for f being Function of L, L st f is monotone for M being Subset
of L st M = {x where x is Element of L: x = f.x} holds subrelstr M is complete
LATTICE;
theorem :: YELLOW_2:30
for S being infs-inheriting non empty full SubRelStr of L holds
S is complete LATTICE;
theorem :: YELLOW_2:31
for S being sups-inheriting non empty full SubRelStr of L holds
S is complete LATTICE;
theorem :: YELLOW_2:32 ::Remark 2.4 (Part I, variant 1)
for M being non empty RelStr for f being Function of L, M st f
is sups-preserving holds Image f is sups-inheriting;
theorem :: YELLOW_2:33 ::Remark 2.4 (Part I, variant 2)
for M being non empty RelStr for f being Function of L, M st f
is infs-preserving holds Image f is infs-inheriting;
theorem :: YELLOW_2:34 ::Remark 2.4 (Part II)
for L, M being complete LATTICE for f being Function of L, M st f is
sups-preserving or f is infs-preserving holds Image f is complete LATTICE;
theorem :: YELLOW_2:35 ::Remark 2.5
for f being Function of L, L st f is idempotent
directed-sups-preserving holds Image f is directed-sups-inheriting & Image f is
complete LATTICE;
begin :: A Lattice of Ideals
theorem :: YELLOW_2:36
for L being RelStr for F being Subset-Family of L st for X being
Subset of L st X in F holds X is lower holds meet F is lower Subset of L;
theorem :: YELLOW_2:37
for L being RelStr for F being Subset-Family of L st for X being
Subset of L st X in F holds X is upper holds meet F is upper Subset of L;
theorem :: YELLOW_2:38
for L being with_suprema antisymmetric RelStr for F being
Subset-Family of L st for X being Subset of L st X in F holds X is lower
directed holds meet F is directed Subset of L;
theorem :: YELLOW_2:39
for L being with_infima antisymmetric RelStr for F being Subset-Family
of L st for X being Subset of L st X in F holds X is upper filtered holds meet
F is filtered Subset of L;
theorem :: YELLOW_2:40
for L being with_infima Poset for I, J being Ideal of L holds I
/\ J is Ideal of L;
registration
let L be non empty reflexive transitive RelStr;
cluster Ids L -> non empty;
end;
theorem :: YELLOW_2:41
for L being non empty reflexive transitive RelStr holds (x is
Element of InclPoset(Ids L) iff x is Ideal of L);
theorem :: YELLOW_2:42
for L being non empty reflexive transitive RelStr for I being
Element of InclPoset(Ids L) holds x in I implies x is Element of L;
theorem :: YELLOW_2:43
for L being with_infima Poset for x, y being Element of InclPoset(Ids
L) holds x "/\" y = x /\ y;
registration
let L be with_infima Poset;
cluster InclPoset(Ids L) -> with_infima;
end;
theorem :: YELLOW_2:44
for L being with_suprema Poset for x, y being Element of
InclPoset(Ids L) holds ex Z being Subset of L st Z = {z where z is Element of L
: z in x or z in y or ex a, b being Element of L st a in x & b in y & z = a
"\/" b} & ex_sup_of {x, y},InclPoset(Ids L) & x "\/" y = downarrow Z;
registration
let L be with_suprema Poset;
cluster InclPoset(Ids L) -> with_suprema;
end;
theorem :: YELLOW_2:45
for L being lower-bounded sup-Semilattice for X being non empty
Subset of Ids L holds meet X is Ideal of L;
theorem :: YELLOW_2:46
for L being lower-bounded sup-Semilattice for A being non empty
Subset of InclPoset(Ids L) holds ex_inf_of A,InclPoset(Ids L) & inf A = meet A;
theorem :: YELLOW_2:47
for L being with_suprema Poset holds ex_inf_of {},InclPoset(Ids
L) & "/\"({}, InclPoset(Ids L)) = [#]L;
theorem :: YELLOW_2:48
for L being lower-bounded sup-Semilattice holds InclPoset(Ids L) is complete;
registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset(Ids L) -> complete;
end;
begin :: Special Maps
definition
let L be non empty Poset;
func SupMap L -> Function of InclPoset(Ids L), L means
:: YELLOW_2:def 3
for I being Ideal of L holds it.I = sup I;
end;
theorem :: YELLOW_2:49
for L being non empty Poset holds dom SupMap L = Ids L & rng
SupMap L is Subset of L;
theorem :: YELLOW_2:50
for L being non empty Poset holds x in dom SupMap L iff x is Ideal of L;
theorem :: YELLOW_2:51
for L being up-complete non empty Poset holds SupMap L is monotone;
registration
let L be up-complete non empty Poset;
cluster SupMap L -> monotone;
end;
definition
let L be non empty Poset;
func IdsMap L -> Function of L, InclPoset(Ids L) means
:: YELLOW_2:def 4
for x being Element of L holds it.x = downarrow x;
end;
theorem :: YELLOW_2:52
for L being non empty Poset holds IdsMap L is monotone;
registration
let L be non empty Poset;
cluster IdsMap L -> monotone;
end;
begin :: A Family of Elements in a Lattice
definition
let L be non empty RelStr;
let F be Relation;
func \\/(F, L) -> Element of L equals
:: YELLOW_2:def 5
"\/"(rng F, L);
func //\(F, L) -> Element of L equals
:: YELLOW_2:def 6
"/\"(rng F, L);
end;
notation
let J be set, L be non empty RelStr;
let F be Function of J, the carrier of L;
synonym Sup F for \\/(F, L);
synonym Inf F for //\(F, L);
end;
reserve J for non empty set,
j for Element of J;
theorem :: YELLOW_2:53
for F being Function of J, the carrier of L holds F.j <= Sup F & Inf F <= F.j
;
theorem :: YELLOW_2:54
for F being Function of J, the carrier of L holds (for j holds F.j <=
a) implies Sup F <= a;
theorem :: YELLOW_2:55
for F being Function of J, the carrier of L holds (for j holds a <= F.
j) implies a <= Inf F;