:: Properties of Relational Structures, Posets, Lattices and Maps
:: by Mariusz \.Zynel and Czes{\l}aw Byli\'nski
::
:: Received September 20, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

theorem :: YELLOW_2:1
for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= downarrow x iff X is_<=_than x )
proofend;

theorem :: YELLOW_2:2
for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X )
proofend;

theorem :: YELLOW_2:3
for L being transitive antisymmetric with_suprema RelStr
for X, Y being set st ex_sup_of X,L &amp; ex_sup_of Y,L holds
( ex_sup_of X \/ Y,L &amp; "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )
proofend;

theorem :: YELLOW_2:4
for L being transitive antisymmetric with_infima RelStr
for X, Y being set st ex_inf_of X,L &amp; ex_inf_of Y,L holds
( ex_inf_of X \/ Y,L &amp; "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) )
proofend;

begin

theorem Th5: :: YELLOW_2:5
for R being Relation
for X, Y being set st X c= Y holds
R |_2 X c= R |_2 Y
proofend;

theorem :: YELLOW_2:6
for L being RelStr
for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds
the InternalRel of S c= the InternalRel of T
proofend;

theorem Th7: :: YELLOW_2:7
for X being set
for L being non empty RelStr
for S being non empty SubRelStr of L holds
( ( X is directed Subset of S implies X is directed Subset of L ) &amp; ( X is filtered Subset of S implies X is filtered Subset of L ) )
proofend;

theorem :: YELLOW_2:8
for L being non empty RelStr
for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds
for X being Subset of S holds
( X is Subset of T &amp; ( for Y being Subset of T st X = Y holds
( ( X is filtered implies Y is filtered ) &amp; ( X is directed implies Y is directed ) ) ) )
proofend;

begin

definition
let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;
predf <= g means :Def1: :: YELLOW_2:def 1
 for j being set st j in J holds
ex a, b being Element of L st
( a = f . j &amp; b = g . j &amp; a <= b );
end;

:: deftheorem Def1 defines <= YELLOW_2:def_1_:_
 for J being set
for L being RelStr
for f, g being Function of J, the carrier of L holds
( f <= g iff for j being set st j in J holds
ex a, b being Element of L st
( a = f . j &amp; b = g . j &amp; a <= b ) );

notation
let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;
synonym g >= f for f <= g;
end;

theorem :: YELLOW_2:9
for L, M being non empty RelStr
for f, g being Function of L,M holds
( f <= g iff for x being Element of L holds f . x <= g . x )
proofend;

begin

definition
let L, M be non empty RelStr ;
let f be Function of L,M;
func Image f ->  strict full SubRelStr of M equals :: YELLOW_2:def 2
 subrelstr (rng f);
correctness
coherence
subrelstr (rng f) is strict full SubRelStr of M;
;
end;

:: deftheorem  defines Image YELLOW_2:def_2_:_
 for L, M being non empty RelStr
for f being Function of L,M holds Image f = subrelstr (rng f);

theorem :: YELLOW_2:10
for L, M being non empty RelStr
for f being Function of L,M
for y being Element of (Image f) ex x being Element of L st f . x = y
proofend;

registration
let L be non empty RelStr ;
let X be non empty Subset of L;
cluster subrelstr X ->  non empty ;
coherence
 not subrelstr X is empty by YELLOW_0:def_15;
end;

registration
let L, M be non empty RelStr ;
let f be Function of L,M;
cluster Image f ->  non empty strict full ;
coherence
 not Image f is empty
proofend;
end;

begin

theorem :: YELLOW_2:11
for L being non empty RelStr holds id L is monotone
proofend;

theorem :: YELLOW_2:12
for L, M, N being non empty RelStr
for f being Function of L,M
for g being Function of M,N st f is monotone &amp; g is monotone holds
g * f is monotone
proofend;

theorem :: YELLOW_2:13
for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone &amp; x is_<=_than X holds
f . x is_<=_than f .: X
proofend;

theorem :: YELLOW_2:14
for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone &amp; X is_<=_than x holds
f .: X is_<=_than f . x
proofend;

theorem :: YELLOW_2:15
for S, T being non empty RelStr
for f being Function of S,T
for X being directed Subset of S st f is monotone holds
f .: X is directed
proofend;

theorem Th16: :: YELLOW_2:16
for L being with_suprema Poset
for f being Function of L,L st f is directed-sups-preserving holds
f is monotone
proofend;

theorem :: YELLOW_2:17
for L being with_infima Poset
for f being Function of L,L st f is filtered-infs-preserving holds
f is monotone
proofend;

begin

theorem :: YELLOW_2:18
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
for x being Element of S holds f . (f . x) = f . x
proofend;

theorem Th19: :: YELLOW_2:19
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
rng f =  {  x where x is Element of S : x = f . x  }
proofend;

theorem Th20: :: YELLOW_2:20
for X being set
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent &amp; X c= rng f holds
f .: X = X
proofend;

theorem :: YELLOW_2:21
for L being non empty RelStr holds id L is idempotent
proofend;

begin

theorem Th22: :: YELLOW_2:22
for X being set
for L being complete LATTICE
for a being Element of L st a in X holds
( a <= "\/" (X,L) &amp; "/\" (X,L) <= a )
proofend;

theorem Th23: :: YELLOW_2:23
for L being non empty RelStr holds
( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L )
proofend;

theorem Th24: :: YELLOW_2:24
for L being non empty RelStr st ( for X being set holds ex_sup_of X,L ) holds
L is complete
proofend;

theorem Th25: :: YELLOW_2:25
for L being non empty RelStr st ( for X being set holds ex_inf_of X,L ) holds
L is complete
proofend;

theorem Th26: :: YELLOW_2:26
for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
for X being set holds
( ex_inf_of X,L &amp; "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
proofend;

theorem :: YELLOW_2:27
for L being non empty RelStr st ( for A being Subset of L holds ex_sup_of A,L ) holds
for X being set holds
( ex_sup_of X,L &amp; "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
proofend;

theorem Th28: :: YELLOW_2:28
for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
L is complete
proofend;

registration
cluster non empty reflexive transitive antisymmetric upper-bounded up-complete /\-complete  ->  non empty complete for RelStr ;
correctness
coherence
for b1 being non empty Poset st b1 is up-complete &amp; b1 is /\-complete &amp; b1 is upper-bounded holds
b1 is complete ;
;
end;

theorem Th29: :: YELLOW_2:29
for L being complete LATTICE
for f being Function of L,L st f is monotone holds
for M being Subset of L st M =  {  x where x is Element of L : x = f . x  }  holds
subrelstr M is complete LATTICE
proofend;

theorem Th30: :: YELLOW_2:30
for L being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE
proofend;

theorem Th31: :: YELLOW_2:31
for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE
proofend;

theorem Th32: :: YELLOW_2:32
for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is sups-preserving holds
Image f is sups-inheriting
proofend;

theorem Th33: :: YELLOW_2:33
for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting
proofend;

theorem :: YELLOW_2:34
for L, M being complete LATTICE
for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds
Image f is complete LATTICE
proofend;

theorem :: YELLOW_2:35
for L being complete LATTICE
for f being Function of L,L st f is idempotent &amp; f is directed-sups-preserving holds
( Image f is directed-sups-inheriting &amp; Image f is complete LATTICE )
proofend;

begin

theorem Th36: :: YELLOW_2:36
for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is lower ) holds
meet F is lower Subset of L
proofend;

theorem :: YELLOW_2:37
for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is upper ) holds
meet F is upper Subset of L
proofend;

theorem Th38: :: YELLOW_2:38
for L being antisymmetric with_suprema RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is lower &amp; X is directed ) ) holds
meet F is directed Subset of L
proofend;

theorem :: YELLOW_2:39
for L being antisymmetric with_infima RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is upper &amp; X is filtered ) ) holds
meet F is filtered Subset of L
proofend;

theorem Th40: :: YELLOW_2:40
for L being with_infima Poset
for I, J being Ideal of L holds I /\ J is Ideal of L
proofend;

registration
let L be non empty reflexive transitive RelStr ;
cluster Ids L ->  non empty ;
correctness
coherence
not Ids L is empty ;
proofend;
end;

theorem Th41: :: YELLOW_2:41
for x being set
for L being non empty reflexive transitive RelStr holds
( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )
proofend;

theorem Th42: :: YELLOW_2:42
for x being set
for L being non empty reflexive transitive RelStr
for I being Element of (InclPoset (Ids L)) st x in I holds
x is Element of L
proofend;

theorem :: YELLOW_2:43
for L being with_infima Poset
for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y
proofend;

registration
let L be with_infima Poset;
cluster InclPoset (Ids L) ->  with_infima ;
correctness
coherence
InclPoset (Ids L) is with_infima ;
proofend;
end;

theorem Th44: :: YELLOW_2:44
for L being with_suprema Poset
for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st
( Z =  {  z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x &amp; b in y &amp; z = a "\/" b ) )  }  &amp; ex_sup_of {x,y}, InclPoset (Ids L) &amp; x "\/" y = downarrow Z )
proofend;

registration
let L be with_suprema Poset;
cluster InclPoset (Ids L) ->  with_suprema ;
correctness
coherence
InclPoset (Ids L) is with_suprema ;
proofend;
end;

theorem Th45: :: YELLOW_2:45
for L being lower-bounded sup-Semilattice
for X being non empty Subset of (Ids L) holds meet X is Ideal of L
proofend;

theorem Th46: :: YELLOW_2:46
for L being lower-bounded sup-Semilattice
for A being non empty Subset of (InclPoset (Ids L)) holds
( ex_inf_of A, InclPoset (Ids L) &amp; inf A = meet A )
proofend;

theorem Th47: :: YELLOW_2:47
for L being with_suprema Poset holds
( ex_inf_of {} , InclPoset (Ids L) &amp; "/\" ({},(InclPoset (Ids L))) = [#] L )
proofend;

theorem Th48: :: YELLOW_2:48
for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is complete
proofend;

registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset (Ids L) ->  complete ;
correctness
coherence
InclPoset (Ids L) is complete ;
by Th48;
end;

begin

definition
let L be non empty Poset;
func SupMap L ->  Function of (InclPoset (Ids L)),L means :Def3: :: YELLOW_2:def 3
 for I being Ideal of L holds it . I = sup I;
existence
 ex b1 being Function of (InclPoset (Ids L)),L st
for I being Ideal of L holds b1 . I = sup I
proofend;
uniqueness
 for b1, b2 being Function of (InclPoset (Ids L)),L st ( for I being Ideal of L holds b1 . I = sup I ) &amp; ( for I being Ideal of L holds b2 . I = sup I ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines SupMap YELLOW_2:def_3_:_
 for L being non empty Poset
for b2 being Function of (InclPoset (Ids L)),L holds
( b2 = SupMap L iff for I being Ideal of L holds b2 . I = sup I );

theorem Th49: :: YELLOW_2:49
for L being non empty Poset holds
( dom (SupMap L) = Ids L &amp; rng (SupMap L) is Subset of L )
proofend;

theorem :: YELLOW_2:50
for x being set
for L being non empty Poset holds
( x in dom (SupMap L) iff x is Ideal of L )
proofend;

theorem Th51: :: YELLOW_2:51
for L being non empty up-complete Poset holds SupMap L is monotone
proofend;

registration
let L be non empty up-complete Poset;
cluster SupMap L ->  monotone ;
correctness
coherence
SupMap L is monotone ;
by Th51;
end;

definition
let L be non empty Poset;
func IdsMap L ->  Function of L,(InclPoset (Ids L)) means :Def4: :: YELLOW_2:def 4
 for x being Element of L holds it . x = downarrow x;
existence
 ex b1 being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds b1 . x = downarrow x
proofend;
uniqueness
 for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b1 . x = downarrow x ) &amp; ( for x being Element of L holds b2 . x = downarrow x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines IdsMap YELLOW_2:def_4_:_
 for L being non empty Poset
for b2 being Function of L,(InclPoset (Ids L)) holds
( b2 = IdsMap L iff for x being Element of L holds b2 . x = downarrow x );

theorem Th52: :: YELLOW_2:52
for L being non empty Poset holds IdsMap L is monotone
proofend;

registration
let L be non empty Poset;
cluster IdsMap L ->  monotone ;
correctness
coherence
IdsMap L is monotone ;
by Th52;
end;

begin

definition
let L be non empty RelStr ;
let F be Relation;
func \\/ (F,L) ->  Element of L equals :: YELLOW_2:def 5
 "\/" ((rng F),L);
coherence
 "\/" ((rng F),L) is Element of L ;
func //\ (F,L) ->  Element of L equals :: YELLOW_2:def 6
 "/\" ((rng F),L);
coherence
 "/\" ((rng F),L) is Element of L ;
end;

:: deftheorem  defines \\/ YELLOW_2:def_5_:_
 for L being non empty RelStr
for F being Relation holds \\/ (F,L) = "\/" ((rng F),L);

:: deftheorem  defines //\ YELLOW_2:def_6_:_
 for L being non empty RelStr
for F being Relation holds //\ (F,L) = "/\" ((rng F),L);

notation
let J be set ;
let L be non empty RelStr ;
let F be Function of J, the carrier of L;
synonym  Sup F for  \\/ (L,J);
synonym  Inf F for  //\ (L,J);
end;

theorem :: YELLOW_2:53
for L being complete LATTICE
for J being non empty set
for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup &amp; Inf <= F . j )
proofend;

theorem :: YELLOW_2:54
for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a
proofend;

theorem :: YELLOW_2:55
for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
proofend;