environ
vocabularies HIDDEN, WAYBEL_0, ORDINAL2, SUBSET_1, WAYBEL_3, CARD_FIL, XXREAL_0, TARSKI, XBOOLE_0, YELLOW_0, LATTICE3, LATTICES, YELLOW_2, WAYBEL_1, YELLOW_1, RELAT_1, FUNCT_1, STRUCT_0, REWRITE1, PBOOLE, FUNCOP_1, FUNCT_6, CARD_3, FINSEQ_4, ORDERS_2, YELLOW_6, CLASSES1, CLASSES2, ZFMISC_1, FUNCT_5, EQREL_1, FUNCT_2, FINSUB_1, FINSET_1, ORDERS_1, RELAT_2, LATTICE2, CAT_1, XBOOLEAN, PARTFUN1, MEMBER_1, SEQM_3, WAYBEL_5, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_5, FUNCT_6, FUNCOP_1, ORDERS_1, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, CARD_3, PBOOLE, PRALG_1, PRALG_2, MSUALG_3, CLASSES1, CLASSES2, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3, YELLOW_6;
definitions TARSKI, LATTICE3;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, CARD_3, ORDERS_2, FUNCT_6, FUNCOP_1, PBOOLE, PRALG_1, PRALG_2, MSUALG_3, RELAT_1, FINSUB_1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3, CLASSES2, YELLOW_6, CLASSES1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCT_4, ORDERS_1, PARTFUN1;
schemes FUNCT_1, FUNCT_2, MSSUBFAM, DOMAIN_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, YELLOW_6, PRALG_1, RELAT_1;
constructors HIDDEN, FINSUB_1, CLASSES1, CLASSES2, BORSUK_1, LATTICE3, PRALG_1, PRALG_2, MSUALG_3, ORDERS_3, WAYBEL_1, WAYBEL_3, YELLOW_6, FUNCT_5, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities BINOP_1, STRUCT_0;
expansions TARSKI, LATTICE3;
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
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
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;
existence
ex b1 being Function of (dom F), the carrier of L st
for x being object 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 object st x in dom F holds
b1 . x = \\/ ((F . x),L) ) & ( for x being object st x in dom F holds
b2 . x = \\/ ((F . x),L) ) holds
b1 = b2
existence
ex b1 being Function of (dom F), the carrier of L st
for x being object 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 object st x in dom F holds
b1 . x = //\ ((F . x),L) ) & ( for x being object st x in dom F holds
b2 . x = //\ ((F . x),L) ) holds
b1 = b2
end;
Lm7:
for L being complete LATTICE
for J being non empty set
for K being V9() 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) )
Lm8:
for L being complete LATTICE st L is continuous holds
for J being non empty set
for K being V9() 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
Lm9:
for L being complete LATTICE st ( for J being non empty set
for K being V9() 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
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
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 V9() 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) holds
rng (G . j) is finite Subset of (rng ((curry F) . j))
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 V9() 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 object 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 V9() 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X ) holds
L is continuous
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)