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