The abstract of the Mizar article:

Properties of Relational Structures, Posets, Lattices and Maps

by

Mariusz Zynel, and

Czeslaw Bylinski

Received September 20, 1996

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;