Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

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

Back to top