Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Properties of Relational Structures, Posets, Lattices and Maps

by
Mariusz Zynel, and
Czeslaw Bylinski

MML identifier: YELLOW_2
[ Mizar article, MML identifier index ]

```environ

vocabulary ORDERS_1, WAYBEL_0, LATTICE3, RELAT_2, YELLOW_0, BOOLE, LATTICES,
RELAT_1, WELLORD1, CAT_1, QUANTAL1, PRE_TOPC, FUNCT_1, GROUP_6, SEQM_3,
ORDINAL2, BINOP_1, BHSP_3, SETFAM_1, FILTER_2, YELLOW_1, SUBSET_1,
WELLORD2, YELLOW_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
SETFAM_1, LATTICE3, WELLORD1, STRUCT_0, ORDERS_1, PRE_TOPC, QUANTAL1,
ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0, GRCAT_1;
constructors WAYBEL_0, YELLOW_1, TOLER_1, ORDERS_3, QUANTAL1, TOPS_2, GRCAT_1;
clusters STRUCT_0, LATTICE3, RELSET_1, YELLOW_0, YELLOW_1, WAYBEL_0, SUBSET_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Basic Facts

reserve x, X, Y for set;

scheme RelStrSubset{L() -> non empty RelStr, P[set]}:
{x where x is Element of L(): P[x]} is Subset of L();

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

scheme LambdaMD{X, Y() -> non empty RelStr, F(set) -> Element of Y()}:
ex f being map of X(), Y() st for x being Element of X() holds f.x = F(x);

scheme KappaMD{X, Y() -> non empty RelStr, F(set) -> set}:
ex f being map of X(), Y() st for x being Element of X() holds f.x = F(x)
provided
for x being Element of X() holds F(x) is Element of Y();

scheme NonUniqExMD{X, Y() -> non empty RelStr, P[set,set]}:
ex f being map of X(), Y() st for x being Element of X() holds P[x, f.x]
provided
for x being Element of X() ex y being Element of Y() st P[x, y];

definition
let S, T be 1-sorted;
let f be map of S, T;
redefine func rng f -> Subset of T;
end;

theorem :: YELLOW_2:9
for S, T being non empty 1-sorted
for f, g being map of S, T
holds
(for s being Element of S holds f.s = g.s) implies f = g;

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;
synonym g >= f;
end;

theorem :: YELLOW_2:10
for L, M being non empty RelStr, f,g being map 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 map of L, M;
func Image f -> strict full SubRelStr of M equals
:: YELLOW_2:def 2

subrelstr rng f;
end;

theorem :: YELLOW_2:11
for L, M being non empty RelStr
for f being map of L, M
holds
rng f = the carrier of Image f;

theorem :: YELLOW_2:12
for L, M being non empty RelStr
for f being map of L, M
for y being Element of Image f
ex x being Element of L st f.x = y;

definition
let L be non empty RelStr;
let X be non empty Subset of L;
cluster subrelstr X -> non empty;
end;

definition
let L, M be non empty RelStr;
let f be map of L, M;
cluster Image f -> non empty;
end;

begin :: Monotone Maps

theorem :: YELLOW_2:13
for L being non empty RelStr holds id L is monotone;

theorem :: YELLOW_2:14
for L, M, N being non empty RelStr
for f being map of L, M, g being map of M, N
holds
f is monotone & g is monotone implies g*f is monotone;

theorem :: YELLOW_2:15
for L, M being non empty RelStr
for f being map 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:16
for L, M being non empty RelStr
for f being map 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:17
for S, T being non empty RelStr
for f being map of S, T
for X being directed Subset of S
holds
f is monotone implies f.:X is directed;

theorem :: YELLOW_2:18
for L being with_suprema Poset
for f being map of L, L
holds
f is directed-sups-preserving implies f is monotone;

theorem :: YELLOW_2:19
for L being with_infima Poset
for f being map of L, L
holds
f is filtered-infs-preserving implies f is monotone;

begin :: Idempotent Maps

theorem :: YELLOW_2:20
for S being non empty 1-sorted
for f being map of S, S
holds
f is idempotent implies for x being Element of S holds f.(f.x) = f.x;

theorem :: YELLOW_2:21
for S being non empty 1-sorted
for f being map of S, S
holds
f is idempotent implies rng f = {x where x is Element of S: x = f.x};

theorem :: YELLOW_2:22
for S being non empty 1-sorted
for f being map of S, S st f is idempotent
holds
X c= rng f implies f.:X = X;

theorem :: YELLOW_2:23
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:24
a in X implies a <= "\/"(X, L) & "/\"(X, L) <= a;

theorem :: YELLOW_2:25
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:26   ::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:27   ::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:28
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:29
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:30   ::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;

definition
cluster up-complete /\-complete upper-bounded -> complete (non empty Poset);
end;

theorem :: YELLOW_2:31   :: Theorem 2.3 (The Fixed-Point Theorem)
for f being map 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:32
for S being infs-inheriting non empty full SubRelStr of L
holds
S is complete LATTICE;

theorem :: YELLOW_2:33
for S being sups-inheriting non empty full SubRelStr of L
holds
S is complete LATTICE;

theorem :: YELLOW_2:34   ::Remark 2.4 (Part I, variant 1)
for M being non empty RelStr
for f being map of L, M st f is sups-preserving
holds
Image f is sups-inheriting;

theorem :: YELLOW_2:35   ::Remark 2.4  (Part I, variant 2)
for M being non empty RelStr
for f being map of L, M st f is infs-preserving
holds
Image f is infs-inheriting;

theorem :: YELLOW_2:36   ::Remark 2.4  (Part II)
for L, M being complete LATTICE
for f being map of L, M st f is sups-preserving or f is infs-preserving
holds
Image f is complete LATTICE;

theorem :: YELLOW_2:37   ::Remark 2.5
for f being map 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:38
for L being RelStr
for F being Subset of bool the carrier 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:39
for L being RelStr
for F being Subset of bool the carrier 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:40
for L being with_suprema antisymmetric RelStr
for F being Subset of bool the carrier 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:41
for L being with_infima antisymmetric RelStr
for F being Subset of bool the carrier 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:42
for L being with_infima Poset
for I, J being Ideal of L
holds
I /\ J is Ideal of L;

definition
let L be non empty reflexive transitive RelStr;
cluster Ids L -> non empty;
end;

theorem :: YELLOW_2:43
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:44
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:45
for L being with_infima Poset
for x, y being Element of InclPoset(Ids L)
holds
x "/\" y = x /\ y;

definition
let L be with_infima Poset;
cluster InclPoset(Ids L) -> with_infima;
end;

theorem :: YELLOW_2:46
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;

definition
let L be with_suprema Poset;
cluster InclPoset(Ids L) -> with_suprema;
end;

theorem :: YELLOW_2:47
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:48
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:49
for L being with_suprema Poset
holds
ex_inf_of {},InclPoset(Ids L) & "/\"({}, InclPoset(Ids L)) = [#]L;

theorem :: YELLOW_2:50
for L being lower-bounded sup-Semilattice
holds
InclPoset(Ids L) is complete;

definition
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 -> map 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:51
for L being non empty Poset
holds
dom SupMap L = Ids L & rng SupMap L is Subset of L;

theorem :: YELLOW_2:52
for L being non empty Poset
holds
x in dom SupMap L iff x is Ideal of L;

theorem :: YELLOW_2:53
for L being up-complete (non empty Poset) holds SupMap L is monotone;

definition
let L be up-complete (non empty Poset);
cluster SupMap L -> monotone;
end;

definition
let L be non empty Poset;
func IdsMap L -> map 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:54
for L being non empty Poset holds IdsMap L is monotone;

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

definition
let J be set, L be non empty RelStr;
let F be Function of J, the carrier of L;
redefine func \\/(F, L);
synonym Sup F;

redefine func //\(F, L);
synonym Inf F;
end;

definition
let J be non empty set, S be non empty 1-sorted;
let F be Function of J, the carrier of S;
let j be Element of J;
redefine func F.j -> Element of S;
end;

definition
let J be set, S be non empty 1-sorted;
let F be Function of J, the carrier of S;
redefine func rng F -> Subset of S;
end;

reserve J for non empty set,
j for Element of J;

theorem :: YELLOW_2:55
for F being Function of J, the carrier of L
holds
F.j <= Sup F & Inf F <= F.j;

theorem :: YELLOW_2:56
for F being Function of J, the carrier of L
holds
(for j holds F.j <= a) implies Sup F <= a;

theorem :: YELLOW_2:57
for F being Function of J, the carrier of L
holds
(for j holds a <= F.j) implies a <= Inf F;
```