:: WAYBEL_5 semantic presentation :: 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 ) )
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
theorem :: WAYBEL_5:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 ) )
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
theorem :: WAYBEL_5:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: WAYBEL_5:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: WAYBEL_5:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: WAYBEL_5:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th6: :: WAYBEL_5:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: WAYBEL_5:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th8: :: WAYBEL_5:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: WAYBEL_5:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th10: :: WAYBEL_5:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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) )
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
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
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
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
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
end;
:: deftheorem Def1 defines \// WAYBEL_5:def 1 :
:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :
theorem Th11: :: WAYBEL_5:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th12: :: WAYBEL_5:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th13: :: WAYBEL_5:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th14: :: WAYBEL_5:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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) )
theorem Th15: :: WAYBEL_5:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th16: :: WAYBEL_5:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th17: :: WAYBEL_5:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
theorem Th18: :: WAYBEL_5:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
theorem :: WAYBEL_5:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th20: :: WAYBEL_5:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
theorem :: WAYBEL_5:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
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))
theorem Th22: :: WAYBEL_5:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
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
theorem :: WAYBEL_5:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def3 defines completely-distributive WAYBEL_5:def 3 :
theorem Th24: :: WAYBEL_5:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th25: :: WAYBEL_5:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
theorem Th26: :: WAYBEL_5:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th27: :: WAYBEL_5:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: WAYBEL_5:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th29: :: WAYBEL_5:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th30: :: WAYBEL_5:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th31: :: WAYBEL_5:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th32: :: WAYBEL_5:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: WAYBEL_5:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)