The abstract of the Mizar article:

Boolean Posets, Posets under Inclusion and Products of Relational Structures

by

Adam Grabowski, and

Robert Milewski

Received September 20, 1996

MML identifier: YELLOW_1

[ Mizar article, MML identifier index ]

environ

 vocabulary LATTICES, LATTICE3, ORDERS_1, FILTER_1, BOOLE, BHSP_3, WELLORD2,
      RELAT_1, RELAT_2, CAT_1, YELLOW_0, WELLORD1, TARSKI, SETFAM_1, ORDINAL2,
      PRE_TOPC, REALSET1, PRALG_1, FUNCT_1, PBOOLE, FUNCOP_1, CARD_3, RLVECT_2,
      GROUP_1, FUNCT_2, SEQM_3, ORDERS_3, YELLOW_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1,
      SETFAM_1, REALSET1, FUNCT_1, STRUCT_0, TOPS_2, WELLORD2, TOLER_1,
      PARTFUN1, FUNCT_2, ORDERS_1, LATTICES, ORDERS_3, LATTICE3, PRE_TOPC,
      PRE_CIRC, PBOOLE, CARD_3, PRALG_1, YELLOW_0;
 constructors YELLOW_0, WELLORD2, TOLER_1, ORDERS_3, TOPS_2, PRE_CIRC, KNASTER;
 clusters STRUCT_0, LATTICES, LATTICE3, YELLOW_0, ORDERS_1, RELSET_1, CANTOR_1,
      PRE_TOPC, KNASTER, FUNCOP_1, SUBSET_1, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Boolean Posets and Posets under Inclusion

 reserve X for set;

definition let L be Lattice;
 cluster LattPOSet L -> with_suprema with_infima;
end;

definition let L be upper-bounded Lattice;
 cluster LattPOSet L -> upper-bounded;
end;

definition
 let L be lower-bounded Lattice;
 cluster LattPOSet L -> lower-bounded;
end;

definition let L be complete Lattice;
 cluster LattPOSet L -> complete;
end;

definition let X be set;
 redefine func RelIncl X -> Order of X;
end;

definition
 let X be set;
 func InclPoset X -> strict RelStr equals
:: YELLOW_1:def 1
   RelStr(#X, RelIncl X#);
end;

definition
 let X be set;
 cluster InclPoset X -> reflexive antisymmetric transitive;
end;

definition
 let X be non empty set;
 cluster InclPoset X -> non empty;
end;

theorem :: YELLOW_1:1
 the carrier of InclPoset X = X &
  the InternalRel of InclPoset X = RelIncl X;

definition let X be set;
 func BoolePoset X -> strict RelStr equals
:: YELLOW_1:def 2
   LattPOSet BooleLatt X;
end;

definition let X be set;
 cluster BoolePoset X -> non empty reflexive antisymmetric transitive;
end;

definition let X be set;
 cluster BoolePoset X -> complete;
end;

theorem :: YELLOW_1:2
 for x,y be Element of BoolePoset X holds
  x <= y iff x c= y;

theorem :: YELLOW_1:3
 for X be non empty set, x,y be Element of InclPoset X holds
  x <= y iff x c= y;

theorem :: YELLOW_1:4
 BoolePoset X = InclPoset bool X;

theorem :: YELLOW_1:5
   for Y be Subset of bool X holds
  InclPoset Y is full SubRelStr of BoolePoset X;

theorem :: YELLOW_1:6
   for X be non empty set holds
  InclPoset X is with_suprema implies
   for x,y be Element of InclPoset X holds x \/ y c= x "\/" y;

theorem :: YELLOW_1:7
   for X be non empty set holds
  InclPoset X is with_infima implies
  for x,y be Element of InclPoset X holds x "/\" y c= x /\ y;

theorem :: YELLOW_1:8
 for X be non empty set holds
 for x,y be Element of InclPoset X st x \/ y in X holds
  x "\/" y = x \/ y;

theorem :: YELLOW_1:9
 for X be non empty set
 for x,y be Element of InclPoset X st x /\ y in X holds
  x "/\" y = x /\ y;

theorem :: YELLOW_1:10
   for L be RelStr st for x,y be Element of L holds x <= y iff x c= y holds
  the InternalRel of L = RelIncl the carrier of L;

theorem :: YELLOW_1:11
  for X be non empty set st
 (for x,y be set st (x in X & y in X) holds x \/ y in X)
   holds InclPoset X is with_suprema;

theorem :: YELLOW_1:12
   for X be non empty set st
  for x,y be set st (x in X & y in X) holds x /\ y in X holds
   InclPoset X is with_infima;

theorem :: YELLOW_1:13
for X be non empty set holds
  {} in X implies Bottom InclPoset X = {};

theorem :: YELLOW_1:14
 for X be non empty set holds
  union X in X implies Top InclPoset X = union X;

theorem :: YELLOW_1:15
   for X being non empty set holds
  InclPoset X is upper-bounded implies union X in X;

theorem :: YELLOW_1:16
   for X be non empty set holds
  InclPoset X is lower-bounded implies meet X in X;

theorem :: YELLOW_1:17
   for x,y be Element of BoolePoset X holds
  x "\/" y = x \/ y & x "/\" y = x /\ y;

theorem :: YELLOW_1:18
   Bottom BoolePoset X = {};

theorem :: YELLOW_1:19
   Top BoolePoset X = X;

theorem :: YELLOW_1:20
   for Y being non empty Subset of BoolePoset X holds
  inf Y = meet Y;

theorem :: YELLOW_1:21
   for Y being Subset of BoolePoset X holds
  sup Y = union Y;

theorem :: YELLOW_1:22
   for T being non empty TopSpace, X being Subset of InclPoset the topology of
T
  holds sup X = union X;

theorem :: YELLOW_1:23
   for T be non empty TopSpace holds Bottom InclPoset the topology of T = {};

theorem :: YELLOW_1:24
    for T be non empty TopSpace
   holds Top InclPoset the topology of T = the carrier of T;

definition let T be non empty TopSpace;
  cluster InclPoset the topology of T -> complete non trivial;
end;

theorem :: YELLOW_1:25
   for T being TopSpace, F being Subset-Family of T holds
  F is open iff F is Subset of InclPoset the topology of T;

begin  :: Products of Relational Structures

reserve x,y,z for set;

definition let R be Relation;
 attr R is RelStr-yielding means
:: YELLOW_1:def 3
 for v being set st v in rng R holds v is RelStr;
end;

definition
 cluster RelStr-yielding -> 1-sorted-yielding Function;
end;

definition let I be set;
 cluster RelStr-yielding ManySortedSet of I;
end;

definition
 let J be non empty set,
     A be RelStr-yielding ManySortedSet of J,
     j be Element of J;
 redefine func A.j -> RelStr;
end;

definition let I be set;
 let J be RelStr-yielding ManySortedSet of I;
 func product J -> strict RelStr means
:: YELLOW_1:def 4
 the carrier of it = product Carrier J &
  for x,y being Element of it st x in product Carrier J
   holds x <= y iff ex f,g being Function st f = x & g = y &
    for i be set st i in I
     ex R being RelStr, xi,yi being Element of R
       st R = J.i & xi = f.i & yi = g.i & xi <= yi;
end;

definition
 let X be set;
 let L be RelStr;
 cluster X --> L -> RelStr-yielding;
end;

definition
 let I be set;
 let T be RelStr;
 func T|^I -> strict RelStr equals
:: YELLOW_1:def 5
   product (I --> T);
end;

theorem :: YELLOW_1:26
  for J be RelStr-yielding ManySortedSet of {} holds
   product J = RelStr (#{{}}, id {{}}#);

theorem :: YELLOW_1:27
 for Y be RelStr holds
  Y|^{} = RelStr (#{{}}, id {{}}#);

theorem :: YELLOW_1:28
 for X be set, Y be RelStr holds
  Funcs (X, the carrier of Y) = the carrier of Y|^X;

definition let X be set;
 let Y be non empty RelStr;
 cluster Y|^X -> non empty;
end;

definition let X be set;
 let Y be reflexive non empty RelStr;
 cluster Y|^X -> reflexive;
end;

definition let Y be non empty RelStr;
 cluster Y|^{} -> trivial;
end;

definition
 let Y be non empty reflexive RelStr;
 cluster Y|^{} -> with_infima with_suprema antisymmetric;
end;

definition let X be set;
 let Y be transitive non empty RelStr;
 cluster Y|^X -> transitive;
end;

definition let X be set;
 let Y be antisymmetric non empty RelStr;
 cluster Y|^X -> antisymmetric;
end;

definition let X be non empty set;
 let Y be non empty with_infima antisymmetric RelStr;
 cluster Y|^X -> with_infima;
end;

definition let X be non empty set;
 let Y be non empty with_suprema antisymmetric RelStr;
 cluster Y|^X -> with_suprema;
end;

definition let S,T be RelStr;
 func MonMaps (S,T) -> strict full SubRelStr of T|^the carrier of S means
:: YELLOW_1:def 6
     for f being map of S,T holds f in the carrier of it iff
    f in Funcs (the carrier of S, the carrier of T) &
  f is monotone;
end;