:: Boolean Posets, Posets under Inclusion and Products of Relational
:: Structures
:: by Adam Grabowski and Robert Milewski
::
:: 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 LATTICES, LATTICE3, SUBSET_1, STRUCT_0, EQREL_1, XBOOLE_0,
PBOOLE, XXREAL_0, REWRITE1, WELLORD2, RELAT_1, ZFMISC_1, RELAT_2,
ORDERS_2, TARSKI, SETFAM_1, CAT_1, YELLOW_0, WELLORD1, ORDINAL2,
PRE_TOPC, RCOMP_1, PRALG_1, FUNCT_1, FUNCOP_1, CARD_3, RLVECT_2, NEWTON,
FUNCT_2, SEQM_3, ORDERS_3, YELLOW_1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1,
SETFAM_1, FUNCT_1, WELLORD2, ORDERS_1, CARD_3, PBOOLE, TOLER_1, PARTFUN1,
FUNCT_2, STRUCT_0, ORDERS_2, TOPS_2, LATTICES, ORDERS_3, LATTICE3,
PRE_TOPC, FUNCOP_1, PRALG_1, YELLOW_0;
constructors SETFAM_1, WELLORD2, TOLER_1, TOPS_2, LATTICE3, YELLOW_0, PRALG_1,
ORDERS_3, CARD_3, RELSET_1;
registrations SUBSET_1, RELSET_1, PARTFUN1, FUNCOP_1, STRUCT_0, LATTICES,
PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0;
requirements SUBSET, BOOLE;
begin :: Boolean Posets and Posets under Inclusion
reserve X for set;
registration
let L be Lattice;
cluster LattPOSet L -> with_suprema with_infima;
end;
registration
let L be upper-bounded Lattice;
cluster LattPOSet L -> upper-bounded;
end;
registration
let L be lower-bounded Lattice;
cluster LattPOSet L -> lower-bounded;
end;
registration
let L be complete Lattice;
cluster LattPOSet L -> complete;
end;
definition
let X be set;
func InclPoset X -> strict RelStr equals
:: YELLOW_1:def 1
RelStr(#X, RelIncl X#);
end;
registration
let X be set;
cluster InclPoset X -> reflexive antisymmetric transitive;
end;
registration
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;
registration
let X be set;
cluster BoolePoset X -> non empty reflexive antisymmetric transitive;
end;
registration
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-Family of 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;
registration
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;
registration
cluster RelStr-yielding -> 1-sorted-yielding for Function;
end;
registration
let I be set;
cluster RelStr-yielding for 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 object 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;
registration
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;
registration
let X be set;
let Y be non empty RelStr;
cluster Y|^X -> non empty;
end;
registration
let X be set;
let Y be reflexive non empty RelStr;
cluster Y|^X -> reflexive;
end;
registration
let Y be non empty RelStr;
cluster Y|^{} -> 1-element;
end;
registration
let Y be non empty reflexive RelStr;
cluster Y|^{} -> with_infima with_suprema antisymmetric;
end;
registration
let X be set;
let Y be transitive non empty RelStr;
cluster Y|^X -> transitive;
end;
registration
let X be set;
let Y be antisymmetric non empty RelStr;
cluster Y|^X -> antisymmetric;
end;
registration
let X be non empty set;
let Y be non empty with_infima antisymmetric RelStr;
cluster Y|^X -> with_infima;
end;
registration
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 Function 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;