:: WAYBEL_5 semantic presentation

Lemma1: for b1 being continuous Semilattice
for b2 being Element of b1 holds
( waybelow b2 is Ideal of b1 & b2 <= sup (waybelow b2) & ( for b3 being Ideal of b1 st b2 <= sup b3 holds
waybelow b2 c= b3 ) )
proof end;

Lemma2: for b1 being up-complete Semilattice st ( for b2 being Element of b1 holds
( waybelow b2 is Ideal of b1 & b2 <= sup (waybelow b2) & ( for b3 being Ideal of b1 st b2 <= sup b3 holds
waybelow b2 c= b3 ) ) ) holds
b1 is continuous
proof end;

theorem Th1: :: WAYBEL_5:1
for b1 being up-complete Semilattice holds
( b1 is continuous iff for b2 being Element of b1 holds
( waybelow b2 is Ideal of b1 & b2 <= sup (waybelow b2) & ( for b3 being Ideal of b1 st b2 <= sup b3 holds
waybelow b2 c= b3 ) ) ) by Lemma1, Lemma2;

Lemma3: for b1 being up-complete Semilattice st b1 is continuous holds
for b2 being Element of b1 ex b3 being Ideal of b1 st
( b2 <= sup b3 & ( for b4 being Ideal of b1 st b2 <= sup b4 holds
b3 c= b4 ) )
proof end;

Lemma4: for b1 being up-complete Semilattice st ( for b2 being Element of b1 ex b3 being Ideal of b1 st
( b2 <= sup b3 & ( for b4 being Ideal of b1 st b2 <= sup b4 holds
b3 c= b4 ) ) ) holds
b1 is continuous
proof end;

theorem Th2: :: WAYBEL_5:2
for b1 being up-complete Semilattice holds
( b1 is continuous iff for b2 being Element of b1 ex b3 being Ideal of b1 st
( b2 <= sup b3 & ( for b4 being Ideal of b1 st b2 <= sup b4 holds
b3 c= b4 ) ) ) by Lemma3, Lemma4;

theorem Th3: :: WAYBEL_5:3
for b1 being lower-bounded continuous sup-Semilattice holds SupMap b1 has_a_lower_adjoint
proof end;

theorem Th4: :: WAYBEL_5:4
for b1 being lower-bounded up-complete LATTICE st SupMap b1 is upper_adjoint holds
b1 is continuous
proof end;

theorem Th5: :: WAYBEL_5:5
for b1 being complete Semilattice st SupMap b1 is infs-preserving & SupMap b1 is sups-preserving holds
SupMap b1 has_a_lower_adjoint
proof end;

definition
let c1, c2 be set ;
let c3 be ManySortedSet of c1;
mode DoubleIndexedSet of a3,a2 is ManySortedFunction of a3,a1 --> a2;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be 1-sorted ;
mode DoubleIndexedSet of a2,a3 is DoubleIndexedSet of a2,the carrier of a3;
end;

theorem Th6: :: WAYBEL_5:6
for b1, b2 being set
for b3 being ManySortedSet of b1
for b4 being DoubleIndexedSet of b3,b2
for b5 being set st b5 in b1 holds
b4 . b5 is Function of b3 . b5,b2
proof end;

definition
let c1, c2 be non empty set ;
let c3 be ManySortedSet of c1;
let c4 be DoubleIndexedSet of c3,c2;
let c5 be Element of c1;
redefine func . as c4 . c5 -> Function of a3 . a5,a2;
coherence
c4 . c5 is Function of c3 . c5,c2 by Th6;
end;

registration
let c1, c2 be non empty set ;
let c3 be V7 ManySortedSet of c1;
let c4 be DoubleIndexedSet of c3,c2;
let c5 be Element of c1;
cluster rng (a4 . a5) -> non empty ;
correctness
coherence
not rng (c4 . c5) is empty;
proof end;
end;

registration
let c1 be set ;
let c2 be non empty set ;
let c3 be V7 ManySortedSet of c1;
cluster -> V7 ManySortedFunction of a3,a1 --> a2;
correctness
coherence
for b1 being DoubleIndexedSet of c3,c2 holds b1 is non-empty;
proof end;
end;

theorem Th7: :: WAYBEL_5:7
for b1 being Function-yielding Function
for b2 being set st b2 in dom (Frege b1) holds
b2 is Function
proof end;

theorem Th8: :: WAYBEL_5:8
for b1 being Function-yielding Function
for b2 being Function st b2 in dom (Frege b1) holds
( dom b2 = dom b1 & dom b1 = dom ((Frege b1) . b2) )
proof end;

theorem Th9: :: WAYBEL_5:9
for b1 being Function-yielding Function
for b2 being Function st b2 in dom (Frege b1) holds
for b3 being set st b3 in dom b1 holds
( b2 . b3 in dom (b1 . b3) & ((Frege b1) . b2) . b3 = (b1 . b3) . (b2 . b3) & (b1 . b3) . (b2 . b3) in rng ((Frege b1) . b2) )
proof end;

theorem Th10: :: WAYBEL_5:10
for b1, b2 being set
for b3 being ManySortedSet of b1
for b4 being DoubleIndexedSet of b3,b2
for b5 being Function st b5 in dom (Frege b4) holds
(Frege b4) . b5 is Function of b1,b2
proof end;

Lemma10: for b1, b2 being set
for b3 being ManySortedSet of b1
for b4 being DoubleIndexedSet of b3,b2
for b5 being Function st b5 in dom (Frege b4) holds
for b6 being set st b6 in b1 holds
( ((Frege b4) . b5) . b6 = (b4 . b6) . (b5 . b6) & (b4 . b6) . (b5 . b6) in rng ((Frege b4) . b5) )
proof end;

Lemma11: for b1 being set
for b2 being ManySortedSet of b1
for b3 being non empty set
for b4 being DoubleIndexedSet of b2,b3
for b5 being Function st b5 in dom (Frege b4) holds
for b6 being set st b6 in b1 holds
b5 . b6 in b2 . b6
proof end;

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

definition
let c1, c2 be set ;
let c3 be ManySortedSet of c1;
let c4 be DoubleIndexedSet of c3,c2;
redefine func Frege as Frege c4 -> DoubleIndexedSet of (product (doms a4)) --> a1,a2;
coherence
Frege c4 is DoubleIndexedSet of (product (doms c4)) --> c1,c2
proof end;
end;

definition
let c1, c2 be non empty set ;
let c3 be V7 ManySortedSet of c1;
let c4 be DoubleIndexedSet of c3,c2;
let c5 be DoubleIndexedSet of (product (doms c4)) --> c1,c2;
let c6 be Element of product (doms c4);
redefine func . as c5 . c6 -> Function of a1,a2;
coherence
c5 . c6 is Function of c1,c2
proof end;
end;

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

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

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

notation
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be non empty RelStr ;
let c4 be DoubleIndexedSet of c2,c3;
synonym Sups c4 for \// c2,c1;
synonym Infs c4 for /\\ c2,c1;
end;

notation
let c1, c2 be set ;
let c3 be non empty RelStr ;
let c4 be DoubleIndexedSet of c1 --> c2,c3;
synonym Sups c4 for \// c2,c1;
synonym Infs c4 for /\\ c2,c1;
end;

theorem Th11: :: WAYBEL_5:11
for b1 being non empty RelStr
for b2, b3 being Function-yielding Function st dom b2 = dom b3 & ( for b4 being set st b4 in dom b2 holds
\\/ (b2 . b4),b1 = \\/ (b3 . b4),b1 ) holds
\// b2,b1 = \// b3,b1
proof end;

theorem Th12: :: WAYBEL_5:12
for b1 being non empty RelStr
for b2, b3 being Function-yielding Function st dom b2 = dom b3 & ( for b4 being set st b4 in dom b2 holds
//\ (b2 . b4),b1 = //\ (b3 . b4),b1 ) holds
/\\ b2,b1 = /\\ b3,b1
proof end;

theorem Th13: :: WAYBEL_5:13
for b1 being set
for b2 being non empty RelStr
for b3 being Function-yielding Function holds
( ( b1 in rng (\// b3,b2) implies ex b4 being set st
( b4 in dom b3 & b1 = \\/ (b3 . b4),b2 ) ) & ( ex b4 being set st
( b4 in dom b3 & b1 = \\/ (b3 . b4),b2 ) implies b1 in rng (\// b3,b2) ) & ( b1 in rng (/\\ b3,b2) implies ex b4 being set st
( b4 in dom b3 & b1 = //\ (b3 . b4),b2 ) ) & ( ex b4 being set st
( b4 in dom b3 & b1 = //\ (b3 . b4),b2 ) implies b1 in rng (/\\ b3,b2) ) )
proof end;

theorem Th14: :: WAYBEL_5:14
for b1 being set
for b2 being non empty RelStr
for b3 being non empty set
for b4 being ManySortedSet of b3
for b5 being DoubleIndexedSet of b4,b2 holds
( ( b1 in rng (Sups ) implies ex b6 being Element of b3 st b1 = Sup ) & ( ex b6 being Element of b3 st b1 = Sup implies b1 in rng (Sups ) ) & ( b1 in rng (Infs ) implies ex b6 being Element of b3 st b1 = Inf ) & ( ex b6 being Element of b3 st b1 = Inf implies b1 in rng (Infs ) ) )
proof end;

registration
let c1 be non empty set ;
let c2 be ManySortedSet of c1;
let c3 be non empty RelStr ;
let c4 be DoubleIndexedSet of c2,c3;
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;

Lemma18: for b1 being complete LATTICE
for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1
for b5 being set holds
( b5 is Element of product (doms b4) iff b5 in dom (Frege b4) )
proof end;

theorem Th15: :: WAYBEL_5:15
for b1 being complete LATTICE
for b2 being Element of b1
for b3 being Function-yielding Function st ( for b4 being Function st b4 in dom (Frege b3) holds
//\ ((Frege b3) . b4),b1 <= b2 ) holds
Sup <= b2
proof end;

theorem Th16: :: WAYBEL_5:16
for b1 being complete LATTICE
for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 holds Inf >= Sup
proof end;

theorem Th17: :: WAYBEL_5:17
for b1 being complete LATTICE
for b2, b3 being Element of b1 st b1 is continuous & ( for b4 being Element of b1 st b4 << b2 holds
b4 <= b3 ) holds
b2 <= b3
proof end;

Lemma22: for b1 being complete LATTICE st b1 is continuous holds
for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 st ( for b5 being Element of b2 holds rng (b4 . b5) is directed ) holds
Inf = Sup
proof end;

theorem Th18: :: WAYBEL_5:18
for b1 being complete LATTICE st ( for b2 being non empty set st b2 in the_universe_of the carrier of b1 holds
for b3 being V7 ManySortedSet of b2 st ( for b4 being Element of b2 holds b3 . b4 in the_universe_of the carrier of b1 ) holds
for b4 being DoubleIndexedSet of b3,b1 st ( for b5 being Element of b2 holds rng (b4 . b5) is directed ) holds
Inf = Sup ) holds
b1 is continuous
proof end;

Lemma24: for b1 being complete LATTICE st ( for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 st ( for b5 being Element of b2 holds rng (b4 . b5) is directed ) holds
Inf = Sup ) holds
b1 is continuous
proof end;

theorem Th19: :: WAYBEL_5:19
for b1 being complete LATTICE holds
( b1 is continuous iff for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 st ( for b5 being Element of b2 holds rng (b4 . b5) is directed ) holds
Inf = Sup ) by Lemma22, Lemma24;

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of [:c1,c2:],c3;
redefine func curry as curry c4 -> DoubleIndexedSet of a1 --> a2,a3;
coherence
curry c4 is DoubleIndexedSet of c1 --> c2,c3
proof end;
end;

theorem Th20: :: WAYBEL_5:20
for b1, b2, b3 being non empty set
for b4 being Element of b1
for b5 being Element of b2
for b6 being Function of [:b1,b2:],b3 holds
( dom (curry b6) = b1 & dom ((curry b6) . b4) = b2 & b6 . [b4,b5] = ((curry b6) . b4) . b5 )
proof end;

Lemma26: for b1 being complete LATTICE st ( for b2, b3 being non empty set
for b4 being Function of [:b2,b3:],the carrier of b1 st ( for b5 being Element of b2 holds rng ((curry b4) . b5) is directed ) holds
Inf = Sup ) holds
b1 is continuous
proof end;

theorem Th21: :: WAYBEL_5:21
for b1 being complete LATTICE holds
( b1 is continuous iff for b2, b3 being non empty set
for b4 being Function of [:b2,b3:],the carrier of b1 st ( for b5 being Element of b2 holds rng ((curry b4) . b5) is directed ) holds
Inf = Sup ) by Lemma22, Lemma26;

Lemma27: for b1, b2 being non empty set
for b3 being Function st b3 in Funcs b1,(Fin b2) holds
for b4 being Element of b1 holds b3 . b4 is finite Subset of b2
proof end;

Lemma28: for b1 being complete LATTICE
for b2, b3, b4 being non empty set
for b5 being Element of b2
for b6 being Function of [:b2,b3:],b4
for b7 being V7 ManySortedSet of b2 st b7 in Funcs b2,(Fin b3) holds
for b8 being DoubleIndexedSet of b7,b1 st ( for b9 being Element of b2
for b10 being set st b10 in b7 . b9 holds
(b8 . b9) . b10 = b6 . [b9,b10] ) holds
rng (b8 . b5) is finite Subset of (rng ((curry b6) . b5))
proof end;

theorem Th22: :: WAYBEL_5:22
for b1 being complete LATTICE
for b2, b3 being non empty set
for b4 being Function of [:b2,b3:],the carrier of b1
for b5 being Subset of b1 st b5 = { b6 where B is Element of b1 : ex b1 being V7 ManySortedSet of b2 st
( b7 in Funcs b2,(Fin b3) & ex b2 being DoubleIndexedSet of b7,b1 st
( ( for b3 being Element of b2
for b4 being set st b10 in b7 . b9 holds
(b8 . b9) . b10 = b4 . [b9,b10] ) & b6 = Inf ) ) } holds
Inf >= sup b5
proof end;

Lemma30: for b1 being complete LATTICE st b1 is continuous holds
for b2, b3 being non empty set
for b4 being Function of [:b2,b3:],the carrier of b1
for b5 being Subset of b1 st b5 = { b6 where B is Element of b1 : ex b1 being V7 ManySortedSet of b2 st
( b7 in Funcs b2,(Fin b3) & ex b2 being DoubleIndexedSet of b7,b1 st
( ( for b3 being Element of b2
for b4 being set st b10 in b7 . b9 holds
(b8 . b9) . b10 = b4 . [b9,b10] ) & b6 = Inf ) ) } holds
Inf = sup b5
proof end;

Lemma31: for b1 being complete LATTICE st ( for b2, b3 being non empty set
for b4 being Function of [:b2,b3:],the carrier of b1
for b5 being Subset of b1 st b5 = { b6 where B is Element of b1 : ex b1 being V7 ManySortedSet of b2 st
( b7 in Funcs b2,(Fin b3) & ex b2 being DoubleIndexedSet of b7,b1 st
( ( for b3 being Element of b2
for b4 being set st b10 in b7 . b9 holds
(b8 . b9) . b10 = b4 . [b9,b10] ) & b6 = Inf ) ) } holds
Inf = sup b5 ) holds
b1 is continuous
proof end;

theorem Th23: :: WAYBEL_5:23
for b1 being complete LATTICE holds
( b1 is continuous iff for b2, b3 being non empty set
for b4 being Function of [:b2,b3:],the carrier of b1
for b5 being Subset of b1 st b5 = { b6 where B is Element of b1 : ex b1 being V7 ManySortedSet of b2 st
( b7 in Funcs b2,(Fin b3) & ex b2 being DoubleIndexedSet of b7,b1 st
( ( for b3 being Element of b2
for b4 being set st b10 in b7 . b9 holds
(b8 . b9) . b10 = b4 . [b9,b10] ) & b6 = Inf ) ) } holds
Inf = sup b5 ) by Lemma30, Lemma31;

definition
let c1 be non empty RelStr ;
attr a1 is completely-distributive means :Def3: :: WAYBEL_5:def 3
( a1 is complete & ( for b1 being non empty set
for b2 being V7 ManySortedSet of b1
for b3 being DoubleIndexedSet of b2,a1 holds Inf = Sup ) );
end;

:: deftheorem Def3 defines completely-distributive WAYBEL_5:def 3 :
for b1 being non empty RelStr holds
( b1 is completely-distributive iff ( b1 is complete & ( for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 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
for b1 being completely-distributive LATTICE holds b1 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
for b1 being non empty transitive antisymmetric with_infima RelStr
for b2 being Element of b1
for b3, b4 being Subset of b1 st ex_sup_of b3,b1 & ex_sup_of b4,b1 & b4 = { (b2 "/\" b5) where B is Element of b1 : b5 in b3 } holds
b2 "/\" (sup b3) >= sup b4
proof end;

Lemma35: for b1 being completely-distributive LATTICE
for b2 being non empty Subset of b1
for b3 being Element of b1 holds b3 "/\" (sup b2) = "\/" { (b3 "/\" b4) where B is Element of b1 : b4 in b2 } ,b1
proof end;

theorem Th26: :: WAYBEL_5:26
for b1 being completely-distributive LATTICE
for b2 being Subset of b1
for b3 being Element of b1 holds b3 "/\" (sup b2) = "\/" { (b3 "/\" b4) where B is Element of b1 : b4 in b2 } ,b1
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 c1 be non empty RelStr ;
mode CLSubFrame of a1 is non empty full infs-inheriting directed-sups-inheriting SubRelStr of a1;
end;

theorem Th27: :: WAYBEL_5:27
for b1 being complete LATTICE
for b2 being non empty set
for b3 being V7 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 st ( for b5 being Element of b2 holds rng (b4 . b5) is directed ) holds
rng (Infs ) is directed
proof end;

theorem Th28: :: WAYBEL_5:28
for b1 being complete LATTICE st b1 is continuous holds
for b2 being CLSubFrame of b1 holds b2 is continuous LATTICE
proof end;

theorem Th29: :: WAYBEL_5:29
for b1 being complete LATTICE
for b2 being non empty Poset st ex b3 being Function of b1,b2 st
( b3 is infs-preserving & b3 is onto ) holds
b2 is complete LATTICE
proof end;

notation
let c1, c2 be set ;
synonym c1 => c2 for c1 --> c2;
end;

notation
let c1, c2 be set ;
synonym c1 => c2 for c1 --> c2;
end;

definition
let c1, c2 be set ;
redefine func => as c1 => c2 -> ManySortedSet of a1;
coherence
c1 => c2 is ManySortedSet of c1
proof end;
end;

definition
let c1, c2, c3 be set ;
let c4 be Function of c1,c2;
redefine func => as c3 => c4 -> ManySortedFunction of a3 --> a1,a3 --> a2;
coherence
c3 => c4 is ManySortedFunction of c3 --> c1,c3 --> c2
proof end;
end;

theorem Th30: :: WAYBEL_5:30
for b1 being non empty set
for b2, b3 being set
for b4 being Function of b2,b3
for b5 being Function of b3,b2 st b5 * b4 = id b2 holds
(b1 => b5) ** (b1 => b4) = id (b1 --> b2)
proof end;

theorem Th31: :: WAYBEL_5:31
for b1, b2 being non empty set
for b3 being set
for b4 being ManySortedSet of b1
for b5 being DoubleIndexedSet of b4,b2
for b6 being Function of b2,b3 holds (b1 => b6) ** b5 is DoubleIndexedSet of b4,b3
proof end;

theorem Th32: :: WAYBEL_5:32
for b1, b2, b3 being non empty set
for b4 being ManySortedSet of b1
for b5 being DoubleIndexedSet of b4,b2
for b6 being Function of b2,b3 holds doms ((b1 => b6) ** b5) = doms b5
proof end;

theorem Th33: :: WAYBEL_5:33
for b1 being complete LATTICE st b1 is continuous holds
for b2 being non empty Poset st ex b3 being Function of b1,b2 st
( b3 is infs-preserving & b3 is directed-sups-preserving & b3 is onto ) holds
b2 is continuous LATTICE
proof end;