:: Boolean Posets, Posets under Inclusion and Products of Relational Structures :: by Adam Grabowski and Robert Milewski :: :: Received September 20, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin registration let L be Lattice; cluster LattPOSet L -> with_suprema with_infima ; coherence ( LattPOSet L is with_suprema & LattPOSet L is with_infima ) by LATTICE3:11; end; registration let L be upper-bounded Lattice; cluster LattPOSet L -> upper-bounded ; coherence LattPOSet L is upper-bounded proofend; end; registration let L be lower-bounded Lattice; cluster LattPOSet L -> lower-bounded ; coherence LattPOSet L is lower-bounded proofend; end; registration let L be complete Lattice; cluster LattPOSet L -> complete ; coherence LattPOSet L is complete proofend; end; definition let X be set ; :: original:RelIncl redefine func RelIncl X -> Order of X; coherence RelIncl X is Order of X proofend; end; definition let X be set ; func InclPoset X -> strict RelStr equals :: YELLOW_1:def 1 RelStr(# X,(RelIncl X) #); correctness coherence RelStr(# X,(RelIncl X) #) is strict RelStr ; ; end; :: deftheorem defines InclPoset YELLOW_1:def_1_:_ for X being set holds InclPoset X = RelStr(# X,(RelIncl X) #); registration let X be set ; cluster InclPoset X -> strict reflexive transitive antisymmetric ; coherence ( InclPoset X is reflexive & InclPoset X is antisymmetric & InclPoset X is transitive ) ; end; registration let X be non empty set ; cluster InclPoset X -> non empty strict ; coherence not InclPoset X is empty ; end; theorem :: YELLOW_1:1 for X being set holds ( 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); correctness coherence LattPOSet (BooleLatt X) is strict RelStr ; ; end; :: deftheorem defines BoolePoset YELLOW_1:def_2_:_ for X being set holds BoolePoset X = LattPOSet (BooleLatt X); registration let X be set ; cluster BoolePoset X -> non empty strict reflexive transitive antisymmetric ; coherence ( not BoolePoset X is empty & BoolePoset X is reflexive & BoolePoset X is antisymmetric & BoolePoset X is transitive ) ; end; registration let X be set ; cluster BoolePoset X -> strict complete ; coherence BoolePoset X is complete ; end; theorem Th2: :: YELLOW_1:2 for X being set for x, y being Element of (BoolePoset X) holds ( x <= y iff x c= y ) proofend; theorem Th3: :: YELLOW_1:3 for X being non empty set for x, y being Element of (InclPoset X) holds ( x <= y iff x c= y ) proofend; theorem Th4: :: YELLOW_1:4 for X being set holds BoolePoset X = InclPoset (bool X) proofend; theorem :: YELLOW_1:5 for X being set for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X proofend; theorem :: YELLOW_1:6 for X being non empty set st InclPoset X is with_suprema holds for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y proofend; theorem :: YELLOW_1:7 for X being non empty set st InclPoset X is with_infima holds for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y proofend; theorem Th8: :: YELLOW_1:8 for X being non empty set for x, y being Element of (InclPoset X) st x \/ y in X holds x "\/" y = x \/ y proofend; theorem Th9: :: YELLOW_1:9 for X being non empty set for x, y being Element of (InclPoset X) st x /\ y in X holds x "/\" y = x /\ y proofend; theorem :: YELLOW_1:10 for L being RelStr st ( for x, y being Element of L holds ( x <= y iff x c= y ) ) holds the InternalRel of L = RelIncl the carrier of L proofend; theorem :: YELLOW_1:11 for X being non empty set st ( for x, y being set st x in X & y in X holds x \/ y in X ) holds InclPoset X is with_suprema proofend; theorem :: YELLOW_1:12 for X being non empty set st ( for x, y being set st x in X & y in X holds x /\ y in X ) holds InclPoset X is with_infima proofend; theorem Th13: :: YELLOW_1:13 for X being non empty set st {} in X holds Bottom (InclPoset X) = {} proofend; theorem Th14: :: YELLOW_1:14 for X being non empty set st union X in X holds Top (InclPoset X) = union X proofend; theorem :: YELLOW_1:15 for X being non empty set st InclPoset X is upper-bounded holds union X in X proofend; theorem :: YELLOW_1:16 for X being non empty set st InclPoset X is lower-bounded holds meet X in X proofend; Lm1: for X being set for x, y being Element of (BoolePoset X) holds ( x /\ y in bool X & x \/ y in bool X ) proofend; theorem :: YELLOW_1:17 for X being set for x, y being Element of (BoolePoset X) holds ( x "\/" y = x \/ y & x "/\" y = x /\ y ) proofend; theorem :: YELLOW_1:18 for X being set holds Bottom (BoolePoset X) = {} proofend; theorem :: YELLOW_1:19 for X being set holds Top (BoolePoset X) = X proofend; theorem :: YELLOW_1:20 for X being set for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y proofend; theorem :: YELLOW_1:21 for X being set for Y being Subset of (BoolePoset X) holds sup Y = union Y proofend; theorem :: YELLOW_1:22 for T being non empty TopSpace for X being Subset of (InclPoset the topology of T) holds sup X = union X proofend; theorem :: YELLOW_1:23 for T being non empty TopSpace holds Bottom (InclPoset the topology of T) = {} by Th13, PRE_TOPC:1; Lm2: for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded proofend; theorem :: YELLOW_1:24 for T being non empty TopSpace holds Top (InclPoset the topology of T) = the carrier of T proofend; Lm3: for T being non empty TopSpace holds InclPoset the topology of T is complete proofend; Lm4: for T being non empty TopSpace holds not InclPoset the topology of T is trivial proofend; registration let T be non empty TopSpace; cluster InclPoset the topology of T -> non trivial strict complete ; coherence ( InclPoset the topology of T is complete & not InclPoset the topology of T is trivial ) by Lm3, Lm4; end; theorem :: YELLOW_1:25 for T being TopSpace for F being Subset-Family of T holds ( F is open iff F is Subset of (InclPoset the topology of T) ) proofend; begin definition let R be Relation; attrR is RelStr-yielding means :Def3: :: YELLOW_1:def 3 for v being set st v in rng R holds v is RelStr ; end; :: deftheorem Def3 defines RelStr-yielding YELLOW_1:def_3_:_ for R being Relation holds ( R is RelStr-yielding iff for v being set st v in rng R holds v is RelStr ); registration cluster Relation-like Function-like RelStr-yielding -> 1-sorted-yielding for set ; coherence for b1 being Function st b1 is RelStr-yielding holds b1 is 1-sorted-yielding proofend; end; registration let I be set ; cluster Relation-like I -defined Function-like V34(I) RelStr-yielding for set ; existence ex b1 being ManySortedSet of I st b1 is RelStr-yielding proofend; end; definition let J be non empty set ; let A be RelStr-yielding ManySortedSet of J; let j be Element of J; :: original:. redefine funcA . j -> RelStr ; coherence A . j is RelStr proofend; end; definition let I be set ; let J be RelStr-yielding ManySortedSet of I; func product J -> strict RelStr means :Def4: :: 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 being set st i in I holds ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ); existence ex b1 being strict RelStr st ( the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds ( x <= y iff ex f, g being Function st ( f = x & g = y & ( for i being set st i in I holds ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) proofend; uniqueness for b1, b2 being strict RelStr st the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds ( x <= y iff ex f, g being Function st ( f = x & g = y & ( for i being set st i in I holds ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of b2 = product (Carrier J) & ( for x, y being Element of b2 st x in product (Carrier J) holds ( x <= y iff ex f, g being Function st ( f = x & g = y & ( for i being set st i in I holds ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines product YELLOW_1:def_4_:_ for I being set for J being RelStr-yielding ManySortedSet of I for b3 being strict RelStr holds ( b3 = product J iff ( the carrier of b3 = product (Carrier J) & ( for x, y being Element of b3 st x in product (Carrier J) holds ( x <= y iff ex f, g being Function st ( f = x & g = y & ( for i being set st i in I holds ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) ); registration let X be set ; let L be RelStr ; clusterX --> L -> RelStr-yielding ; coherence X --> L is RelStr-yielding proofend; end; definition let I be set ; let T be RelStr ; funcT |^ I -> strict RelStr equals :: YELLOW_1:def 5 product (I --> T); correctness coherence product (I --> T) is strict RelStr ; ; end; :: deftheorem defines |^ YELLOW_1:def_5_:_ for I being set for T being RelStr holds T |^ I = product (I --> T); theorem Th26: :: YELLOW_1:26 for J being RelStr-yielding ManySortedSet of {} holds product J = RelStr(# {{}},(id {{}}) #) proofend; theorem :: YELLOW_1:27 for Y being RelStr holds Y |^ {} = RelStr(# {{}},(id {{}}) #) by Th26; theorem Th28: :: YELLOW_1:28 for X being set for Y being RelStr holds Funcs (X, the carrier of Y) = the carrier of (Y |^ X) proofend; registration let X be set ; let Y be non empty RelStr ; clusterY |^ X -> non empty strict ; coherence not Y |^ X is empty proofend; end; Lm5: for X being set for Y being non empty RelStr for x being Element of (Y |^ X) holds ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y ) proofend; registration let X be set ; let Y be non empty reflexive RelStr ; clusterY |^ X -> strict reflexive ; coherence Y |^ X is reflexive proofend; end; registration let Y be non empty RelStr ; clusterY |^ {} -> 1 -element strict ; coherence Y |^ {} is 1 -element by Th26; end; registration let Y be non empty reflexive RelStr ; clusterY |^ {} -> strict antisymmetric with_suprema with_infima ; coherence ( Y |^ {} is with_infima & Y |^ {} is with_suprema & Y |^ {} is antisymmetric ) ; end; registration let X be set ; let Y be non empty transitive RelStr ; clusterY |^ X -> strict transitive ; coherence Y |^ X is transitive proofend; end; registration let X be set ; let Y be non empty antisymmetric RelStr ; clusterY |^ X -> strict antisymmetric ; coherence Y |^ X is antisymmetric proofend; end; registration let X be non empty set ; let Y be non empty antisymmetric with_infima RelStr ; clusterY |^ X -> strict with_infima ; coherence Y |^ X is with_infima proofend; end; registration let X be non empty set ; let Y be non empty antisymmetric with_suprema RelStr ; clusterY |^ X -> strict with_suprema ; coherence Y |^ X is with_suprema proofend; 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 ) ); existence ex b1 being strict full SubRelStr of T |^ the carrier of S st for f being Function of S,T holds ( f in the carrier of b1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) proofend; uniqueness for b1, b2 being strict full SubRelStr of T |^ the carrier of S st ( for f being Function of S,T holds ( f in the carrier of b1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) & ( for f being Function of S,T holds ( f in the carrier of b2 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) holds b1 = b2 proofend; end; :: deftheorem defines MonMaps YELLOW_1:def_6_:_ for S, T being RelStr for b3 being strict full SubRelStr of T |^ the carrier of S holds ( b3 = MonMaps (S,T) iff for f being Function of S,T holds ( f in the carrier of b3 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) );