:: 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 )
proof end;

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 )
proof end;

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

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

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
proof end;

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
proof end;

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 ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )
proof end;

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 & ( for Y being Subset of T st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
proof end;

begin

definition
let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;
pred f <= 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 & b = g . j & 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 & b = g . j & 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 )
proof end;

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
proof end;

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
proof end;
end;

begin

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

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 & g is monotone holds
g * f is monotone
proof end;

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 & x is_<=_than X holds
f . x is_<=_than f .: X
proof end;

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 & X is_<=_than x holds
f .: X is_<=_than f . x
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 }
proof end;

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 & X c= rng f holds
f .: X = X
proof end;

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

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) & "/\" (X,L) <= a )
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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 & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
proof end;

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 & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
proof end;

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
proof end;

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 & b1 is /\-complete & 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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

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
proof end;

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
proof end;

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 & X is directed ) ) holds
meet F is directed Subset of L
proof end;

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 & X is filtered ) ) holds
meet F is filtered Subset of L
proof end;

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
proof end;

registration
let L be non empty reflexive transitive RelStr ;
cluster Ids L -> non empty ;
correctness
coherence
not Ids L is empty
;
proof end;
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 )
proof end;

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
proof end;

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

registration
let L be with_infima Poset;
cluster InclPoset (Ids L) -> with_infima ;
correctness
coherence
InclPoset (Ids L) is with_infima
;
proof end;
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 & b in y & z = a "\/" b ) )
}
& ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )
proof end;

registration
let L be with_suprema Poset;
cluster InclPoset (Ids L) -> with_suprema ;
correctness
coherence
InclPoset (Ids L) is with_suprema
;
proof end;
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
proof end;

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) & inf A = meet A )
proof end;

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

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

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
proof end;
uniqueness
for b1, b2 being Function of (InclPoset (Ids L)),L st ( for I being Ideal of L holds b1 . I = sup I ) & ( for I being Ideal of L holds b2 . I = sup I ) holds
b1 = b2
proof end;
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 & rng (SupMap L) is Subset of L )
proof end;

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 )
proof end;

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

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
proof end;
uniqueness
for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b1 . x = downarrow x ) & ( for x being Element of L holds b2 . x = downarrow x ) holds
b1 = b2
proof end;
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
proof end;

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 & Inf <= F . j )
proof end;

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
proof end;

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
proof end;