:: YELLOW_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: YELLOW_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th5: :: YELLOW_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

definition
let S, T be 1-sorted ;
let f be Function of S,T;
:: original: rng
redefine func rng f -> Subset of T;
coherence
rng f is Subset of T
by RELSET_1:12;
end;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: YELLOW_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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 Th11: :: YELLOW_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L, M being non empty RelStr
for f being Function of L,M holds rng f = the carrier of (Image f) by YELLOW_0:def 15;

theorem :: YELLOW_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;
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;

theorem :: YELLOW_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr holds id L is monotone
proof end;

theorem :: YELLOW_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th18: :: YELLOW_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: YELLOW_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th21: :: YELLOW_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th22: :: YELLOW_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr holds id L is idempotent
proof end;

theorem Th24: :: YELLOW_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th25: :: YELLOW_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th26: :: YELLOW_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr st ( for X being set holds ex_sup_of X,L ) holds
L is complete
proof end;

theorem Th27: :: YELLOW_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr st ( for X being set holds ex_inf_of X,L ) holds
L is complete
proof end;

theorem Th28: :: YELLOW_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th30: :: YELLOW_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm1: for L being non empty Poset st L is up-complete & L is /\-complete & L is upper-bounded holds
L is non empty complete Poset
proof end;

registration
cluster non empty upper-bounded up-complete /\-complete -> non empty complete 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
;
by Lm1;
end;

theorem Th31: :: YELLOW_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th32: :: YELLOW_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE
proof end;

theorem Th33: :: YELLOW_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE
proof end;

theorem Th34: :: YELLOW_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th35: :: YELLOW_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th38: :: YELLOW_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th40: :: YELLOW_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th42: :: YELLOW_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th43: :: YELLOW_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th44: :: YELLOW_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th46: :: YELLOW_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th47: :: YELLOW_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th48: :: YELLOW_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th49: :: YELLOW_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset holds
( ex_inf_of {} , InclPoset (Ids L) & "/\" {} ,(InclPoset (Ids L)) = [#] L )
proof end;

theorem Th50: :: YELLOW_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) -> with_suprema complete ;
correctness
coherence
InclPoset (Ids L) is complete
;
by Th50;
end;

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 Th51: :: YELLOW_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Poset holds
( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L )
proof end;

theorem :: YELLOW_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th53: :: YELLOW_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th53;
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 Th54: :: YELLOW_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th54;
end;

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;

definition
let J be non empty set ;
let S be non empty 1-sorted ;
let F be Function of J,the carrier of S;
let j be Element of J;
:: original: .
redefine func F . j -> Element of S;
coherence
F . j is Element of S
proof end;
end;

definition
let J be set ;
let S be non empty 1-sorted ;
let F be Function of J,the carrier of S;
:: original: rng
redefine func rng F -> Subset of S;
coherence
rng F is Subset of S
by RELSET_1:12;
end;

theorem :: YELLOW_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;