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

theorem Th1: :: WAYBEL20:1  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 Subset of (id X) holds proj1 S = proj2 S
proof end;

theorem Th2: :: WAYBEL20:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty set
for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X
proof end;

definition
let L1, L2, T1, T2 be RelStr ;
let f be Function of L1,T1;
let g be Function of L2,T2;
:: original: [:
redefine func [:f,g:] -> Function of [:L1,L2:],[:T1,T2:];
coherence
[:f,g:] is Function of [:L1,L2:],[:T1,T2:]
proof end;
end;

theorem Th3: :: WAYBEL20:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function
for X being set holds
( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )
proof end;

theorem Th4: :: WAYBEL20:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function
for X being set st X c= [:(dom f),(dom g):] holds
( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )
proof end;

theorem Th5: :: WAYBEL20:5  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 antisymmetric RelStr st ex_inf_of {} ,S holds
S is upper-bounded
proof end;

theorem Th6: :: WAYBEL20:6  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 antisymmetric RelStr st ex_sup_of {} ,S holds
S is lower-bounded
proof end;

theorem Th7: :: WAYBEL20:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
proof end;

theorem Th8: :: WAYBEL20:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
proof end;

theorem Th9: :: WAYBEL20:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds
[:f,g:] is infs-preserving
proof end;

theorem :: WAYBEL20:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving
proof end;

theorem :: WAYBEL20:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds
[:f,g:] is sups-preserving
proof end;

theorem Th12: :: WAYBEL20:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving
proof end;

theorem Th13: :: WAYBEL20: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 antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds
inf X in id the carrier of L
proof end;

theorem Th14: :: WAYBEL20:14  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 antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds
sup X in id the carrier of L
proof end;

theorem Th15: :: WAYBEL20: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 st L,M are_isomorphic & L is reflexive holds
M is reflexive
proof end;

theorem Th16: :: WAYBEL20: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 st L,M are_isomorphic & L is transitive holds
M is transitive
proof end;

theorem Th17: :: WAYBEL20:17  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 st L,M are_isomorphic & L is antisymmetric holds
M is antisymmetric
proof end;

theorem Th18: :: WAYBEL20:18  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 st L,M are_isomorphic & L is complete holds
M is complete
proof end;

theorem Th19: :: WAYBEL20:19  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 transitive RelStr
for k being Function of L,L st k is infs-preserving holds
corestr k is infs-preserving
proof end;

theorem :: WAYBEL20:20  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 transitive RelStr
for k being Function of L,L st k is filtered-infs-preserving holds
corestr k is filtered-infs-preserving
proof end;

theorem :: WAYBEL20:21  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 transitive RelStr
for k being Function of L,L st k is sups-preserving holds
corestr k is sups-preserving
proof end;

theorem Th22: :: WAYBEL20:22  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 transitive RelStr
for k being Function of L,L st k is directed-sups-preserving holds
corestr k is directed-sups-preserving
proof end;

theorem :: WAYBEL20:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: WAYBEL20:24  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 reflexive antisymmetric RelStr
for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone
proof end;

theorem Th25: :: WAYBEL20:25  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 st f is monotone holds
for X being Subset of S st X is filtered holds
f .: X is filtered
proof end;

theorem Th26: :: WAYBEL20:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds
g * f is infs-preserving
proof end;

theorem :: WAYBEL20:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
proof end;

theorem :: WAYBEL20:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
proof end;

theorem :: WAYBEL20:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
proof end;

theorem :: WAYBEL20:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
product J is lower-bounded
proof end;

theorem :: WAYBEL20:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
product J is upper-bounded
proof end;

theorem :: WAYBEL20:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)
proof end;

theorem :: WAYBEL20:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)
proof end;

theorem :: WAYBEL20:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous
proof end;

theorem Th35: :: WAYBEL20:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L, T being complete continuous LATTICE
for g being CLHomomorphism of L,T
for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
proof end;

definition
let L be RelStr ;
let R be Subset of [:L,L:];
assume A1: R is Equivalence_Relation of the carrier of L ;
func EqRel R -> Equivalence_Relation of the carrier of L equals :Def1: :: WAYBEL20:def 1
R;
correctness
coherence
R is Equivalence_Relation of the carrier of L
;
by A1;
end;

:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :
for L being RelStr
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds
EqRel R = R;

definition
let L be non empty RelStr ;
let R be Subset of [:L,L:];
attr R is CLCongruence means :Def2: :: WAYBEL20:def 2
( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] );
end;

:: deftheorem Def2 defines CLCongruence WAYBEL20:def 2 :
for L being non empty RelStr
for R being Subset of [:L,L:] holds
( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) );

theorem Th36: :: WAYBEL20:36  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 R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being Element of L holds [(inf (Class (EqRel R),x)),x] in R
proof end;

definition
let L be complete LATTICE;
let R be non empty Subset of [:L,L:];
assume A1: R is CLCongruence ;
func kernel_op R -> kernel Function of L,L means :Def3: :: WAYBEL20:def 3
for x being Element of L holds it . x = inf (Class (EqRel R),x);
existence
ex b1 being kernel Function of L,L st
for x being Element of L holds b1 . x = inf (Class (EqRel R),x)
proof end;
uniqueness
for b1, b2 being kernel Function of L,L st ( for x being Element of L holds b1 . x = inf (Class (EqRel R),x) ) & ( for x being Element of L holds b2 . x = inf (Class (EqRel R),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :
for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b3 being kernel Function of L,L holds
( b3 = kernel_op R iff for x being Element of L holds b3 . x = inf (Class (EqRel R),x) );

theorem Th37: :: WAYBEL20: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 R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
proof end;

theorem Th38: :: WAYBEL20:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for R being Subset of [:L,L:]
for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class (EqRel R),x ) holds
g is CLHomomorphism of L,LR ) )
proof end;

theorem Th39: :: WAYBEL20:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class (EqRel R),x ) holds
g is CLHomomorphism of L,LR ) ) holds
subrelstr R is CLSubFrame of [:L,L:]
proof end;

registration
let L be non empty reflexive RelStr ;
cluster directed-sups-preserving kernel Relation of the carrier of L,the carrier of L;
existence
ex b1 being Function of L,L st
( b1 is directed-sups-preserving & b1 is kernel )
proof end;
end;

definition
let L be non empty reflexive RelStr ;
let k be kernel Function of L,L;
func kernel_congruence k -> non empty Subset of [:L,L:] equals :: WAYBEL20:def 4
[:k,k:] " (id the carrier of L);
coherence
[:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:]
proof end;
end;

:: deftheorem defines kernel_congruence WAYBEL20:def 4 :
for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L);

theorem Th40: :: WAYBEL20:40  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 reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k is Equivalence_Relation of the carrier of L by Th2;

theorem Th41: :: WAYBEL20:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence
proof end;

definition
let L be complete continuous LATTICE;
let R be non empty Subset of [:L,L:];
assume A1: R is CLCongruence ;
func L ./. R -> strict complete continuous LATTICE means :Def5: :: WAYBEL20:def 5
( the carrier of it = Class (EqRel R) & ( for x, y being Element of it holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) );
existence
ex b1 being strict complete continuous LATTICE st
( the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) )
proof end;
uniqueness
for b1, b2 being strict complete continuous LATTICE st the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) & the carrier of b2 = Class (EqRel R) & ( for x, y being Element of b2 holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ./. WAYBEL20:def 5 :
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b3 being strict complete continuous LATTICE holds
( b3 = L ./. R iff ( the carrier of b3 = Class (EqRel R) & ( for x, y being Element of b3 holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) ) );

theorem :: WAYBEL20:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class (EqRel R),y )
proof end;

theorem :: WAYBEL20:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
R = kernel_congruence (kernel_op R) by Th37;

theorem :: WAYBEL20:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)
proof end;

theorem :: WAYBEL20:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete continuous LATTICE
for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
proof end;