:: Boolean Posets, Posets under Inclusion and Products of Relational Structures
:: by Adam Grabowski and Robert Milewski
::
:: Received September 20, 1996
:: Copyright (c) 1996-2011 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

proof end;

end;

registration

let L be lower-bounded Lattice;
cluster LattPOSet L -> lower-bounded ;
coherence
LattPOSet L is lower-bounded

proof end;

end;

registration

let L be complete Lattice;
cluster LattPOSet L -> complete ;
coherence
LattPOSet L is complete

proof end;

end;

definition

let X be set ;
:: original: RelIncl
redefine func RelIncl X -> Order of X;
coherence
RelIncl X is Order of X

proof end;

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 )

proof end;

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 )

proof end;

theorem Th4: :: YELLOW_1:4

for X being set holds BoolePoset X = InclPoset (bool X)

proof end;

theorem :: YELLOW_1:5

for X being set
for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th13: :: YELLOW_1:13

for X being non empty set st {} in X holds
Bottom (InclPoset X) = {}

proof end;

theorem Th14: :: YELLOW_1:14

for X being non empty set st union X in X holds
Top (InclPoset X) = union X

proof end;

theorem :: YELLOW_1:15

for X being non empty set st InclPoset X is upper-bounded holds
union X in X

proof end;

theorem :: YELLOW_1:16

for X being non empty set st InclPoset X is lower-bounded holds
meet X in X

proof end;

Lm1: for X being set
for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )

proof end;

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 )

proof end;

theorem :: YELLOW_1:18

for X being set holds Bottom (BoolePoset X) = {}

proof end;

theorem :: YELLOW_1:19

for X being set holds Top (BoolePoset X) = X

proof end;

theorem :: YELLOW_1:20

for X being set
for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y

proof end;

theorem :: YELLOW_1:21

for X being set
for Y being Subset of (BoolePoset X) holds sup Y = union Y

proof end;

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

proof end;

theorem :: YELLOW_1:23

for T being non empty TopSpace holds Bottom (InclPoset the topology of T) = {} by Th13, PRE_TOPC:5;

Lm2: for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded

proof end;

theorem :: YELLOW_1:24

for T being non empty TopSpace holds Top (InclPoset the topology of T) = the carrier of T

proof end;

Lm3: for T being non empty TopSpace holds InclPoset the topology of T is complete

proof end;

Lm4: for T being non empty TopSpace holds not InclPoset the topology of T is trivial

proof end;

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) )

proof end;

begin

definition

let R be Relation;
attr R 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 set ;
coherence
for b₁ being Function st b₁ is RelStr-yielding holds
b₁ is 1-sorted-yielding

proof end;

end;

registration

let I be set ;
cluster Relation-like I -defined Function-like V34(I) RelStr-yielding set ;
existence
ex b₁ being ManySortedSet of I st b₁ is RelStr-yielding

proof end;

end;

definition

let J be non empty set ;
let A be RelStr-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> RelStr ;
coherence
A . j is RelStr

proof end;

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 b₁ being strict RelStr st
( the carrier of b₁ = product (Carrier J) & ( for x, y being Element of b₁ 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 ) ) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = product (Carrier J) & ( for x, y being Element of b₁ 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 b₂ = product (Carrier J) & ( for x, y being Element of b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines product YELLOW_1:def 4 :
for I being set
for J being RelStr-yielding ManySortedSet of I
for b₃ being strict RelStr holds
( b₃ = product J iff ( the carrier of b₃ = product (Carrier J) & ( for x, y being Element of b₃ 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 ;
cluster X --> L -> RelStr-yielding ;
coherence
X --> L is RelStr-yielding

proof end;

end;

definition

let I be set ;
let T be RelStr ;
func T |^ 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 {{}}) #)

proof end;

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)

proof end;

registration

let X be set ;
let Y be non empty RelStr ;
cluster Y |^ X -> non empty strict ;
coherence
not Y |^ X is empty

proof end;

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 )

proof end;

registration

let X be set ;
let Y be non empty reflexive RelStr ;
cluster Y |^ X -> strict reflexive ;
coherence
Y |^ X is reflexive

proof end;

end;

registration

let Y be non empty RelStr ;
cluster Y |^ {} -> trivial strict ;
coherence
Y |^ {} is trivial by Th26;

end;

registration

let Y be non empty reflexive RelStr ;
cluster Y |^ {} -> 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 ;
cluster Y |^ X -> strict transitive ;
coherence
Y |^ X is transitive

proof end;

end;

registration

let X be set ;
let Y be non empty antisymmetric RelStr ;
cluster Y |^ X -> strict antisymmetric ;
coherence
Y |^ X is antisymmetric

proof end;

end;

registration

let X be non empty set ;
let Y be non empty antisymmetric with_infima RelStr ;
cluster Y |^ X -> strict with_infima ;
coherence
Y |^ X is with_infima

proof end;

end;

registration

let X be non empty set ;
let Y be non empty antisymmetric with_suprema RelStr ;
cluster Y |^ X -> strict with_suprema ;
coherence
Y |^ X is with_suprema

proof end;

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 b₁ being strict full SubRelStr of T |^ the carrier of S st
for f being Function of S,T holds
( f in the carrier of b₁ iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )

proof end;

uniqueness
for b₁, b₂ being strict full SubRelStr of T |^ the carrier of S st ( for f being Function of S,T holds
( f in the carrier of b₁ 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 b₂ iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines MonMaps YELLOW_1:def 6 :
for S, T being RelStr
for b₃ being strict full SubRelStr of T |^ the carrier of S holds
( b₃ = MonMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b₃ iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) );