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

Lm1: for L being continuous Semilattice
for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) )
proof end;

Lm2: for L being up-complete Semilattice st ( for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) ) ) holds
L is continuous
proof end;

theorem :: WAYBEL_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being up-complete Semilattice holds
( L is continuous iff for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) ) ) by Lm1, Lm2;

Lm3: for L being up-complete Semilattice st L is continuous holds
for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
proof end;

Lm4: for L being up-complete Semilattice st ( for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) ) holds
L is continuous
proof end;

theorem :: WAYBEL_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being up-complete Semilattice holds
( L is continuous iff for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) ) by Lm3, Lm4;

theorem :: WAYBEL_5:3  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 continuous sup-Semilattice holds SupMap L has_a_lower_adjoint
proof end;

theorem :: WAYBEL_5:4  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 up-complete LATTICE st SupMap L is upper_adjoint holds
L is continuous
proof end;

theorem :: WAYBEL_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Semilattice st SupMap L is infs-preserving & SupMap L is sups-preserving holds
SupMap L has_a_lower_adjoint
proof end;

definition
let J, D be set ;
let K be ManySortedSet of J;
mode DoubleIndexedSet of K,D is ManySortedFunction of K,J --> D;
end;

definition
let J be set ;
let K be ManySortedSet of J;
let S be 1-sorted ;
mode DoubleIndexedSet of K,S is DoubleIndexedSet of K,the carrier of S;
end;

theorem Th6: :: WAYBEL_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J, D being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for j being set st j in J holds
F . j is Function of K . j,D
proof end;

definition
let J, D be non empty set ;
let K be ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
:: original: .
redefine func F . j -> Function of K . j,D;
coherence
F . j is Function of K . j,D
by Th6;
end;

registration
let J, D be non empty set ;
let K be V7 ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
cluster rng (F . j) -> non empty ;
correctness
coherence
not rng (F . j) is empty
;
proof end;
end;

registration
let J be set ;
let D be non empty set ;
let K be V7 ManySortedSet of J;
cluster -> V7 ManySortedFunction of K,J --> D;
correctness
coherence
for b1 being DoubleIndexedSet of K,D holds b1 is non-empty
;
proof end;
end;

theorem Th7: :: WAYBEL_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function-yielding Function
for f being set st f in dom (Frege F) holds
f is Function
proof end;

theorem Th8: :: WAYBEL_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function-yielding Function
for f being Function st f in dom (Frege F) holds
( dom f = dom F & dom F = dom ((Frege F) . f) )
proof end;

theorem Th9: :: WAYBEL_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function-yielding Function
for f being Function st f in dom (Frege F) holds
for i being set st i in dom F holds
( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
proof end;

theorem Th10: :: WAYBEL_5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J, D being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D
proof end;

Lm5: for J, D being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
proof end;

Lm6: for J being set
for K being ManySortedSet of J
for D being non empty set
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
f . j in K . j
proof end;

registration
let f be non-empty Function;
cluster doms f -> non-empty ;
correctness
coherence
doms f is non-empty
;
proof end;
end;

definition
let J, D be set ;
let K be ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
:: original: Frege
redefine func Frege F -> DoubleIndexedSet of (product (doms F)) --> J,D;
coherence
Frege F is DoubleIndexedSet of (product (doms F)) --> J,D
proof end;
end;

definition
let J, D be non empty set ;
let K be V7 ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let G be DoubleIndexedSet of (product (doms F)) --> J,D;
let f be Element of product (doms F);
:: original: .
redefine func G . f -> Function of J,D;
coherence
G . f is Function of J,D
proof end;
end;

definition
let L be non empty RelStr ;
let F be Function-yielding Function;
func \// F,L -> Function of dom F,the carrier of L means :Def1: :: WAYBEL_5:def 1
for x being set st x in dom F holds
it . x = \\/ (F . x),L;
existence
ex b1 being Function of dom F,the carrier of L st
for x being set st x in dom F holds
b1 . x = \\/ (F . x),L
proof end;
uniqueness
for b1, b2 being Function of dom F,the carrier of L st ( for x being set st x in dom F holds
b1 . x = \\/ (F . x),L ) & ( for x being set st x in dom F holds
b2 . x = \\/ (F . x),L ) holds
b1 = b2
proof end;
func /\\ F,L -> Function of dom F,the carrier of L means :Def2: :: WAYBEL_5:def 2
for x being set st x in dom F holds
it . x = //\ (F . x),L;
existence
ex b1 being Function of dom F,the carrier of L st
for x being set st x in dom F holds
b1 . x = //\ (F . x),L
proof end;
uniqueness
for b1, b2 being Function of dom F,the carrier of L st ( for x being set st x in dom F holds
b1 . x = //\ (F . x),L ) & ( for x being set st x in dom F holds
b2 . x = //\ (F . x),L ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines \// WAYBEL_5:def 1 :
for L being non empty RelStr
for F being Function-yielding Function
for b3 being Function of dom F,the carrier of L holds
( b3 = \// F,L iff for x being set st x in dom F holds
b3 . x = \\/ (F . x),L );

:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :
for L being non empty RelStr
for F being Function-yielding Function
for b3 being Function of dom F,the carrier of L holds
( b3 = /\\ F,L iff for x being set st x in dom F holds
b3 . x = //\ (F . x),L );

notation
let J be set ;
let K be ManySortedSet of J;
let L be non empty RelStr ;
let F be DoubleIndexedSet of K,L;
synonym Sups F for \// K,J;
synonym Infs F for /\\ K,J;
end;

notation
let I, J be set ;
let L be non empty RelStr ;
let F be DoubleIndexedSet of I --> J,L;
synonym Sups F for \// J,I;
synonym Infs F for /\\ J,I;
end;

theorem Th11: :: WAYBEL_5:11  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 F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds
\\/ (F . x),L = \\/ (G . x),L ) holds
\// F,L = \// G,L
proof end;

theorem Th12: :: WAYBEL_5:12  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 F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds
//\ (F . x),L = //\ (G . x),L ) holds
/\\ F,L = /\\ G,L
proof end;

theorem Th13: :: WAYBEL_5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set
for L being non empty RelStr
for F being Function-yielding Function holds
( ( y in rng (\// F,L) implies ex x being set st
( x in dom F & y = \\/ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = \\/ (F . x),L ) implies y in rng (\// F,L) ) & ( y in rng (/\\ F,L) implies ex x being set st
( x in dom F & y = //\ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = //\ (F . x),L ) implies y in rng (/\\ F,L) ) )
proof end;

theorem Th14: :: WAYBEL_5:14  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 J being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,L holds
( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )
proof end;

registration
let J be non empty set ;
let K be ManySortedSet of J;
let L be non empty RelStr ;
let F be DoubleIndexedSet of K,L;
cluster rng (Sups ) -> non empty ;
correctness
coherence
not rng (Sups ) is empty
;
proof end;
cluster rng (Infs ) -> non empty ;
correctness
coherence
not rng (Infs ) is empty
;
proof end;
end;

Lm7: for L being complete LATTICE
for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L
for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )
proof end;

theorem Th15: :: WAYBEL_5:15  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 F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds
//\ ((Frege F) . f),L <= a ) holds
Sup <= a
proof end;

theorem Th16: :: WAYBEL_5:16  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 K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup
proof end;

theorem Th17: :: WAYBEL_5:17  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, b being Element of L st L is continuous & ( for c being Element of L st c << a holds
c <= b ) holds
a <= b
proof end;

Lm8: for L being complete LATTICE st L is continuous holds
for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
proof end;

theorem Th18: :: WAYBEL_5:18  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 st ( for J being non empty set st J in the_universe_of the carrier of L holds
for K being V7 ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) holds
L is continuous
proof end;

Lm9: for L being complete LATTICE st ( for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) holds
L is continuous
proof end;

theorem :: WAYBEL_5:19  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 holds
( L is continuous iff for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) by Lm8, Lm9;

definition
let J, K, D be non empty set ;
let F be Function of [:J,K:],D;
:: original: curry
redefine func curry F -> DoubleIndexedSet of J --> K,D;
coherence
curry F is DoubleIndexedSet of J --> K,D
proof end;
end;

theorem Th20: :: WAYBEL_5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J, K, D being non empty set
for j being Element of J
for k being Element of K
for F being Function of [:J,K:],D holds
( dom (curry F) = J & dom ((curry F) . j) = K & F . [j,k] = ((curry F) . j) . k )
proof end;

Lm10: for L being complete LATTICE st ( for J, K being non empty set
for F being Function of [:J,K:],the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup ) holds
L is continuous
proof end;

theorem :: WAYBEL_5:21  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 holds
( L is continuous iff for J, K being non empty set
for F being Function of [:J,K:],the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup ) by Lm8, Lm10;

Lm11: for J, K being non empty set
for f being Function st f in Funcs J,(Fin K) holds
for j being Element of J holds f . j is finite Subset of K
proof end;

Lm12: for L being complete LATTICE
for J, K, D being non empty set
for j being Element of J
for F being Function of [:J,K:],D
for f being V7 ManySortedSet of J st f in Funcs J,(Fin K) holds
for G being DoubleIndexedSet of f,L st ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) holds
rng (G . j) is finite Subset of (rng ((curry F) . j))
proof end;

theorem Th22: :: WAYBEL_5:22  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, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) )
}
holds
Inf >= sup X
proof end;

Lm13: for L being complete LATTICE st L is continuous holds
for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) )
}
holds
Inf = sup X
proof end;

Lm14: for L being complete LATTICE st ( for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) )
}
holds
Inf = sup X ) holds
L is continuous
proof end;

theorem :: WAYBEL_5:23  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 holds
( L is continuous iff for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) )
}
holds
Inf = sup X ) by Lm13, Lm14;

definition
let L be non empty RelStr ;
attr L is completely-distributive means :Def3: :: WAYBEL_5:def 3
( L is complete & ( for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ) );
end;

:: deftheorem Def3 defines completely-distributive WAYBEL_5:def 3 :
for L being non empty RelStr holds
( L is completely-distributive iff ( L is complete & ( for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) );

registration
cluster non empty trivial -> non empty completely-distributive RelStr ;
coherence
for b1 being non empty Poset st b1 is trivial holds
b1 is completely-distributive
proof end;
end;

registration
cluster completely-distributive RelStr ;
existence
ex b1 being LATTICE st b1 is completely-distributive
proof end;
end;

theorem Th24: :: WAYBEL_5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being completely-distributive LATTICE holds L is continuous
proof end;

registration
cluster completely-distributive -> complete continuous RelStr ;
correctness
coherence
for b1 being LATTICE st b1 is completely-distributive holds
( b1 is complete & b1 is continuous )
;
by Def3, Th24;
end;

theorem Th25: :: WAYBEL_5: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 transitive antisymmetric with_infima RelStr
for x being Element of L
for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds
x "/\" (sup X) >= sup Y
proof end;

Lm15: for L being completely-distributive LATTICE
for X being non empty Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L
proof end;

theorem Th26: :: WAYBEL_5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being completely-distributive LATTICE
for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L
proof end;

registration
cluster completely-distributive -> Heyting RelStr ;
correctness
coherence
for b1 being LATTICE st b1 is completely-distributive holds
b1 is Heyting
;
proof end;
end;

definition
let L be non empty RelStr ;
mode CLSubFrame of L is non empty full infs-inheriting directed-sups-inheriting SubRelStr of L;
end;

theorem Th27: :: WAYBEL_5:27  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 K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
proof end;

theorem :: WAYBEL_5:28  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 st L is continuous holds
for S being CLSubFrame of L holds S is continuous LATTICE
proof end;

theorem Th29: :: WAYBEL_5:29  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 Poset st ex g being Function of L,S st
( g is infs-preserving & g is onto ) holds
S is complete LATTICE
proof end;

notation
let J, y be set ;
synonym J => y for J --> y;
end;

notation
let J, y be set ;
synonym J => y for J --> y;
end;

definition
let J, y be set ;
:: original: =>
redefine func J => y -> ManySortedSet of J;
coherence
J => y is ManySortedSet of J
proof end;
end;

definition
let A, B, J be set ;
let f be Function of A,B;
:: original: =>
redefine func J => f -> ManySortedFunction of J --> A,J --> B;
coherence
J => f is ManySortedFunction of J --> A,J --> B
proof end;
end;

theorem Th30: :: WAYBEL_5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J being non empty set
for A, B being set
for f being Function of A,B
for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)
proof end;

theorem Th31: :: WAYBEL_5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J, A being non empty set
for B being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
proof end;

theorem Th32: :: WAYBEL_5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J, A, B being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds doms ((J => f) ** F) = doms F
proof end;

theorem :: WAYBEL_5: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 st L is continuous holds
for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds
S is continuous LATTICE
proof end;