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

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 for set ;
coherence
for b1 being Function st b1 is RelStr-yielding holds
b1 is 1-sorted-yielding
proof end;
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
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 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 ) ) ) ) ) )
proof end;
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
proof end;
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 ;
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 |^ {} -> 1 -element strict ;
coherence
Y |^ {} is 1 -element
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 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 ) )
proof end;
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
proof end;
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 ) ) );