:: WAYBEL_5 semantic presentation
begin
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
let L be continuous Semilattice; ::_thesis: 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 ) )
let x be Element of L; ::_thesis: ( 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 ) )
thus waybelow x is Ideal of L ; ::_thesis: ( x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) )
thus x <= sup (waybelow x) by WAYBEL_3:def_5; ::_thesis: for I being Ideal of L st x <= sup I holds
waybelow x c= I
thus for I being Ideal of L st x <= sup I holds
waybelow x c= I ::_thesis: verum
proof
let I be Ideal of L; ::_thesis: ( x <= sup I implies waybelow x c= I )
assume A1: x <= sup I ; ::_thesis: waybelow x c= I
waybelow x c= I
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in waybelow x or y in I )
assume y in waybelow x ; ::_thesis: y in I
then y in { y9 where y9 is Element of L : y9 << x } by WAYBEL_3:def_3;
then ex y9 being Element of L st
( y = y9 & y9 << x ) ;
hence y in I by A1, WAYBEL_3:20; ::_thesis: verum
end;
hence waybelow x c= I ; ::_thesis: verum
end;
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
let L be up-complete Semilattice; ::_thesis: ( ( 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 ) ) ) implies L is continuous )
assume A1: 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 ) ) ; ::_thesis: L is continuous
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x)
let x be Element of L; ::_thesis: x = sup (waybelow x)
A2: x <= sup (waybelow x) by A1;
( not waybelow x is empty & waybelow x is directed ) by A1;
then A3: ex_sup_of waybelow x,L by WAYBEL_0:75;
waybelow x is_<=_than x by WAYBEL_3:9;
then sup (waybelow x) <= x by A3, YELLOW_0:def_9;
hence x = sup (waybelow x) by A2, YELLOW_0:def_3; ::_thesis: verum
end;
then A4: L is satisfying_axiom_of_approximation by WAYBEL_3:def_5;
for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) by A1;
hence L is continuous by A4, WAYBEL_3:def_6; ::_thesis: verum
end;
theorem :: WAYBEL_5:1
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
let L be up-complete Semilattice; ::_thesis: ( L is continuous implies 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 ) ) )
assume A1: L is continuous ; ::_thesis: 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 ) )
let x be Element of L; ::_thesis: ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
reconsider I = waybelow x as Ideal of L by A1;
take I ; ::_thesis: ( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
thus ( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) by A1, Lm1; ::_thesis: verum
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
let L be up-complete Semilattice; ::_thesis: ( ( 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 ) ) ) implies L is continuous )
assume A1: 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 ) ) ; ::_thesis: L is continuous
now__::_thesis:_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_)_)
let x be Element of L; ::_thesis: ( 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 ) )
consider I being Ideal of L such that
A2: x <= sup I and
A3: for J being Ideal of L st x <= sup J holds
I c= J by A1;
now__::_thesis:_for_y_being_set_st_y_in_I_holds_
y_in_waybelow_x
let y be set ; ::_thesis: ( y in I implies y in waybelow x )
assume A4: y in I ; ::_thesis: y in waybelow x
then reconsider y9 = y as Element of L ;
for J being Ideal of L st x <= sup J holds
y in J
proof
let J be Ideal of L; ::_thesis: ( x <= sup J implies y in J )
assume x <= sup J ; ::_thesis: y in J
then I c= J by A3;
hence y in J by A4; ::_thesis: verum
end;
then y9 << x by WAYBEL_3:21;
hence y in waybelow x by WAYBEL_3:7; ::_thesis: verum
end;
then A5: I c= waybelow x by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_waybelow_x_holds_
y_in_I
let y be set ; ::_thesis: ( y in waybelow x implies y in I )
assume A6: y in waybelow x ; ::_thesis: y in I
then reconsider y9 = y as Element of L ;
y9 << x by A6, WAYBEL_3:7;
hence y in I by A2, WAYBEL_3:20; ::_thesis: verum
end;
then waybelow x c= I by TARSKI:def_3;
then waybelow x = I by A5, XBOOLE_0:def_10;
hence ( 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 A2, A3; ::_thesis: verum
end;
hence L is continuous by Lm2; ::_thesis: verum
end;
theorem :: WAYBEL_5:2
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
for L being lower-bounded continuous sup-Semilattice holds SupMap L is upper_adjoint
proof
let L be lower-bounded continuous sup-Semilattice; ::_thesis: SupMap L is upper_adjoint
set P = InclPoset (Ids L);
set r = SupMap L;
deffunc H1( Element of L) -> Element of the carrier of (InclPoset (Ids L)) = inf ((SupMap L) " (uparrow {$1}));
ex d being Function of L,(InclPoset (Ids L)) st
for t being Element of L holds d . t = H1(t) from FUNCT_2:sch_4();
then consider d being Function of L,(InclPoset (Ids L)) such that
A1: for t being Element of L holds d . t = inf ((SupMap L) " (uparrow {t})) ;
for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t)
proof
let t be Element of L; ::_thesis: d . t is_minimum_of (SupMap L) " (uparrow t)
set I = inf ((SupMap L) " (uparrow t));
reconsider I9 = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:41;
A2: d . t = inf ((SupMap L) " (uparrow {t})) by A1
.= inf ((SupMap L) " (uparrow t)) by WAYBEL_0:def_18 ;
inf ((SupMap L) " (uparrow t)) in the carrier of (InclPoset (Ids L)) ;
then inf ((SupMap L) " (uparrow t)) in Ids L by YELLOW_1:1;
then A3: inf ((SupMap L) " (uparrow t)) in dom (SupMap L) by YELLOW_2:49;
consider J being Ideal of L such that
A4: t <= sup J and
A5: for K being Ideal of L st t <= sup K holds
J c= K by Lm3;
reconsider J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A6: for K being Element of (InclPoset (Ids L)) st (SupMap L) " (uparrow t) is_>=_than K holds
K <= J9
proof
J9 in the carrier of (InclPoset (Ids L)) ;
then J9 in Ids L by YELLOW_1:1;
then A7: J in dom (SupMap L) by YELLOW_2:49;
let K be Element of (InclPoset (Ids L)); ::_thesis: ( (SupMap L) " (uparrow t) is_>=_than K implies K <= J9 )
assume A8: (SupMap L) " (uparrow t) is_>=_than K ; ::_thesis: K <= J9
t <= (SupMap L) . J9 by A4, YELLOW_2:def_3;
then (SupMap L) . J in uparrow t by WAYBEL_0:18;
then J in (SupMap L) " (uparrow t) by A7, FUNCT_1:def_7;
hence K <= J9 by A8, LATTICE3:def_8; ::_thesis: verum
end;
(SupMap L) " (uparrow t) is_>=_than J9
proof
let K be Element of (InclPoset (Ids L)); :: according to LATTICE3:def_8 ::_thesis: ( not K in (SupMap L) " (uparrow t) or J9 <= K )
reconsider K9 = K as Ideal of L by YELLOW_2:41;
assume K in (SupMap L) " (uparrow t) ; ::_thesis: J9 <= K
then (SupMap L) . K in uparrow t by FUNCT_1:def_7;
then t <= (SupMap L) . K by WAYBEL_0:18;
then t <= sup K9 by YELLOW_2:def_3;
then J9 c= K9 by A5;
hence J9 <= K by YELLOW_1:3; ::_thesis: verum
end;
then t <= sup I9 by A4, A6, YELLOW_0:31;
then t <= (SupMap L) . (inf ((SupMap L) " (uparrow t))) by YELLOW_2:def_3;
then (SupMap L) . (inf ((SupMap L) " (uparrow t))) in uparrow t by WAYBEL_0:18;
then ( ex_inf_of (SupMap L) " (uparrow t), InclPoset (Ids L) & inf ((SupMap L) " (uparrow t)) in (SupMap L) " (uparrow t) ) by A3, FUNCT_1:def_7, YELLOW_0:17;
hence d . t is_minimum_of (SupMap L) " (uparrow t) by A2, WAYBEL_1:def_6; ::_thesis: verum
end;
then [(SupMap L),d] is Galois by WAYBEL_1:10;
hence SupMap L is upper_adjoint by WAYBEL_1:def_11; ::_thesis: verum
end;
theorem :: WAYBEL_5:4
for L being lower-bounded up-complete LATTICE st SupMap L is upper_adjoint holds
L is continuous
proof
let L be lower-bounded up-complete LATTICE; ::_thesis: ( SupMap L is upper_adjoint implies L is continuous )
set P = InclPoset (Ids L);
assume A1: SupMap L is upper_adjoint ; ::_thesis: L is continuous
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
set r = SupMap L;
let x be Element of L; ::_thesis: ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
set I9 = inf ((SupMap L) " (uparrow x));
reconsider I = inf ((SupMap L) " (uparrow x)) as Ideal of L by YELLOW_2:41;
A2: for J being Ideal of L st x <= sup J holds
I c= J
proof
let J be Ideal of L; ::_thesis: ( x <= sup J implies I c= J )
reconsider J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41;
assume x <= sup J ; ::_thesis: I c= J
then x <= (SupMap L) . J9 by YELLOW_2:def_3;
then ( J in dom (SupMap L) & (SupMap L) . J9 in uparrow x ) by WAYBEL_0:18, YELLOW_2:50;
then J9 in (SupMap L) " (uparrow x) by FUNCT_1:def_7;
then inf ((SupMap L) " (uparrow x)) <= J9 by YELLOW_2:22;
hence I c= J by YELLOW_1:3; ::_thesis: verum
end;
consider d being Function of L,(InclPoset (Ids L)) such that
A3: [(SupMap L),d] is Galois by A1, WAYBEL_1:def_11;
d . x is_minimum_of (SupMap L) " (uparrow x) by A3, WAYBEL_1:10;
then I in (SupMap L) " (uparrow x) by WAYBEL_1:def_6;
then (SupMap L) . I in uparrow x by FUNCT_1:def_7;
then x <= (SupMap L) . (inf ((SupMap L) " (uparrow x))) by WAYBEL_0:18;
then x <= sup I by YELLOW_2:def_3;
hence 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 A2; ::_thesis: verum
end;
hence L is continuous by Lm4; ::_thesis: verum
end;
theorem :: WAYBEL_5:5
for L being complete Semilattice st SupMap L is infs-preserving & SupMap L is sups-preserving holds
SupMap L is upper_adjoint
proof
let L be complete Semilattice; ::_thesis: ( SupMap L is infs-preserving & SupMap L is sups-preserving implies SupMap L is upper_adjoint )
set r = SupMap L;
assume ( SupMap L is infs-preserving & SupMap L is sups-preserving ) ; ::_thesis: SupMap L is upper_adjoint
then ex d being Function of L,(InclPoset (Ids L)) st
( [(SupMap L),d] is Galois & ( for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t) ) ) by WAYBEL_1:14;
hence SupMap L is upper_adjoint by WAYBEL_1:def_11; ::_thesis: verum
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
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
let J, D be set ; ::_thesis: 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
let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,D
for j being set st j in J holds
F . j is Function of (K . j),D
let F be DoubleIndexedSet of K,D; ::_thesis: for j being set st j in J holds
F . j is Function of (K . j),D
let j be set ; ::_thesis: ( j in J implies F . j is Function of (K . j),D )
assume A1: j in J ; ::_thesis: F . j is Function of (K . j),D
then (J --> D) . j = D by FUNCOP_1:7;
hence F . j is Function of (K . j),D by A1, PBOOLE:def_15; ::_thesis: verum
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 funcF . 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 V9() ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
cluster proj2 (F . j) -> non empty ;
correctness
coherence
not rng (F . j) is empty ;
;
end;
registration
let J be set ;
let D be non empty set ;
let K be V9() ManySortedSet of J;
cluster -> V9() for ManySortedFunction of K,J --> D;
correctness
coherence
for b1 being DoubleIndexedSet of K,D holds b1 is V9();
proof
let F be DoubleIndexedSet of K,D; ::_thesis: F is V9()
for j being set st j in dom F holds
not F . j is empty
proof
let j be set ; ::_thesis: ( j in dom F implies not F . j is empty )
set k = the Element of K . j;
assume j in dom F ; ::_thesis: not F . j is empty
then A1: j in J ;
then F . j is Function of (K . j),D by Th6;
then dom (F . j) = K . j by FUNCT_2:def_1;
then [ the Element of K . j,((F . j) . the Element of K . j)] in F . j by A1, FUNCT_1:def_2;
hence not F . j is empty ; ::_thesis: verum
end;
hence F is V9() by FUNCT_1:def_9; ::_thesis: verum
end;
end;
theorem :: WAYBEL_5:7
for F being Function-yielding Function
for f being set st f in dom (Frege F) holds
f is Function ;
theorem Th8: :: WAYBEL_5:8
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
let F be Function-yielding Function; ::_thesis: for f being Function st f in dom (Frege F) holds
( dom f = dom F & dom F = dom ((Frege F) . f) )
let f be Function; ::_thesis: ( f in dom (Frege F) implies ( dom f = dom F & dom F = dom ((Frege F) . f) ) )
assume f in dom (Frege F) ; ::_thesis: ( dom f = dom F & dom F = dom ((Frege F) . f) )
then A1: f in product (doms F) ;
then ex g being Function st
( g = f & dom g = dom (doms F) & ( for x being set st x in dom (doms F) holds
g . x in (doms F) . x ) ) by CARD_3:def_5;
hence dom f = dom F by FUNCT_6:59; ::_thesis: dom F = dom ((Frege F) . f)
thus dom ((Frege F) . f) = dom (F .. f) by A1, PRALG_2:def_2
.= dom F by PRALG_1:def_17 ; ::_thesis: verum
end;
theorem Th9: :: WAYBEL_5:9
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
let F be Function-yielding Function; ::_thesis: 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) )
let f be Function; ::_thesis: ( f in dom (Frege F) implies 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) ) )
assume A1: f in dom (Frege F) ; ::_thesis: 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) )
A2: f in product (doms F) by A1;
set G = (Frege F) . f;
let i be set ; ::_thesis: ( i in dom F implies ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) )
assume A3: i in dom F ; ::_thesis: ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
i in dom (doms F) by A3, FUNCT_6:59;
then f . i in (doms F) . i by A2, CARD_3:9;
hence f . i in dom (F . i) by A3, FUNCT_6:22; ::_thesis: ( ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
(Frege F) . f = F .. f by A2, PRALG_2:def_2;
hence A4: ((Frege F) . f) . i = (F . i) . (f . i) by A3, PRALG_1:def_17; ::_thesis: (F . i) . (f . i) in rng ((Frege F) . f)
dom ((Frege F) . f) = dom F by A1, Th8;
hence (F . i) . (f . i) in rng ((Frege F) . f) by A3, A4, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th10: :: WAYBEL_5:10
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
let J, D be set ; ::_thesis: 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
let K be ManySortedSet of J; ::_thesis: 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
let F be DoubleIndexedSet of K,D; ::_thesis: for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D
let f be Function; ::_thesis: ( f in dom (Frege F) implies (Frege F) . f is Function of J,D )
assume A1: f in dom (Frege F) ; ::_thesis: (Frege F) . f is Function of J,D
set G = (Frege F) . f;
A2: dom ((Frege F) . f) = dom F by A1, Th8;
A3: dom F = J by PARTFUN1:def_2;
rng ((Frege F) . f) c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((Frege F) . f) or y in D )
assume y in rng ((Frege F) . f) ; ::_thesis: y in D
then consider x being set such that
A4: x in dom ((Frege F) . f) and
A5: y = ((Frege F) . f) . x by FUNCT_1:def_3;
F . x is Function of (K . x),D by A2, A4, Th6;
then A6: rng (F . x) c= D by RELAT_1:def_19;
( ((Frege F) . f) . x = (F . x) . (f . x) & f . x in dom (F . x) ) by A1, A2, A4, Th9;
then y in rng (F . x) by A5, FUNCT_1:def_3;
hence y in D by A6; ::_thesis: verum
end;
hence (Frege F) . f is Function of J,D by A3, A2, FUNCT_2:2; ::_thesis: verum
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
let J, D be set ; ::_thesis: 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) )
let K be ManySortedSet of J; ::_thesis: 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) )
let F be DoubleIndexedSet of K,D; ::_thesis: 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) )
let f be Function; ::_thesis: ( f in dom (Frege F) implies 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) ) )
assume A1: f in dom (Frege F) ; ::_thesis: 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) )
let j be set ; ::_thesis: ( j in J implies ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) )
assume j in J ; ::_thesis: ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
then A2: j in dom F by PARTFUN1:def_2;
hence ((Frege F) . f) . j = (F . j) . (f . j) by A1, Th9; ::_thesis: (F . j) . (f . j) in rng ((Frege F) . f)
thus (F . j) . (f . j) in rng ((Frege F) . f) by A1, A2, Th9; ::_thesis: verum
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
let J be set ; ::_thesis: 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
let K be ManySortedSet of J; ::_thesis: 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
let D be non empty set ; ::_thesis: 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
let F be DoubleIndexedSet of K,D; ::_thesis: 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
let f be Function; ::_thesis: ( f in dom (Frege F) implies for j being set st j in J holds
f . j in K . j )
assume A1: f in dom (Frege F) ; ::_thesis: for j being set st j in J holds
f . j in K . j
let j be set ; ::_thesis: ( j in J implies f . j in K . j )
assume A2: j in J ; ::_thesis: f . j in K . j
A3: F . j is Function of (K . j),D by A2, Th6;
dom F = J by PARTFUN1:def_2;
then f . j in dom (F . j) by A1, A2, Th9;
hence f . j in K . j by A3, FUNCT_2:def_1; ::_thesis: verum
end;
registration
let f be non-empty Function;
cluster doms f -> non-empty ;
correctness
coherence
doms f is non-empty ;
proof
for j being set st j in dom (doms f) holds
not (doms f) . j is empty
proof
let j be set ; ::_thesis: ( j in dom (doms f) implies not (doms f) . j is empty )
assume that
A1: j in dom (doms f) and
A2: (doms f) . j is empty ; ::_thesis: contradiction
A3: j in f " (SubFuncs (rng f)) by A1, FUNCT_6:def_2;
then reconsider fj = f . j as Function by FUNCT_6:19;
A4: j in dom f by A3, FUNCT_6:19;
then {} = dom fj by A2, FUNCT_6:22;
then f . j = {} ;
hence contradiction by A4, FUNCT_1:def_9; ::_thesis: verum
end;
hence doms f is non-empty by FUNCT_1:def_9; ::_thesis: verum
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
set G = Frege F;
set PD = product (doms F);
set A = (product (doms F)) --> J;
set B = (product (doms F)) --> D;
for i being set st i in product (doms F) holds
(Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i)
proof
let i be set ; ::_thesis: ( i in product (doms F) implies (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) )
assume A1: i in product (doms F) ; ::_thesis: (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i)
then reconsider f = i as Function ;
A2: ((product (doms F)) --> D) . i = D by A1, FUNCOP_1:7;
( i in dom (Frege F) & ((product (doms F)) --> J) . i = J ) by A1, FUNCOP_1:7, PARTFUN1:def_2;
then (Frege F) . f is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) by A2, Th10;
hence (Frege F) . i is Function of (((product (doms F)) --> J) . i),(((product (doms F)) --> D) . i) ; ::_thesis: verum
end;
hence Frege F is DoubleIndexedSet of (product (doms F)) --> J,D by PBOOLE:def_15; ::_thesis: verum
end;
end;
definition
let J, D be non empty set ;
let K be V9() 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 funcG . f -> Function of J,D;
coherence
G . f is Function of J,D
proof
((product (doms F)) --> J) . f = J by FUNCOP_1:7;
hence G . f is Function of J,D ; ::_thesis: verum
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
deffunc H1( set ) -> Element of the carrier of L = \\/ ((F . $1),L);
ex f being Function st
( dom f = dom F & ( for x being set st x in dom F holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
then consider f being Function such that
A1: dom f = dom F and
A2: for x being set st x in dom F holds
f . x = \\/ ((F . x),L) ;
rng f c= the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of L )
assume y in rng f ; ::_thesis: y in the carrier of L
then consider x being set such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
y = \\/ ((F . x),L) by A1, A2, A3;
hence y in the carrier of L ; ::_thesis: verum
end;
then reconsider f = f as Function of (dom F), the carrier of L by A1, FUNCT_2:2;
take f ; ::_thesis: for x being set st x in dom F holds
f . x = \\/ ((F . x),L)
thus for x being set st x in dom F holds
f . x = \\/ ((F . x),L) by A2; ::_thesis: verum
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
let f, g be Function of (dom F), the carrier of L; ::_thesis: ( ( for x being set st x in dom F holds
f . x = \\/ ((F . x),L) ) & ( for x being set st x in dom F holds
g . x = \\/ ((F . x),L) ) implies f = g )
assume that
A4: for x being set st x in dom F holds
f . x = \\/ ((F . x),L) and
A5: for x being set st x in dom F holds
g . x = \\/ ((F . x),L) ; ::_thesis: f = g
A6: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom F implies f . x = g . x )
assume A7: x in dom F ; ::_thesis: f . x = g . x
hence f . x = \\/ ((F . x),L) by A4
.= g . x by A5, A7 ;
::_thesis: verum
end;
( dom f = dom F & dom g = dom F ) by FUNCT_2:def_1;
hence f = g by A6, FUNCT_1:2; ::_thesis: verum
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
deffunc H1( set ) -> Element of the carrier of L = //\ ((F . $1),L);
ex f being Function st
( dom f = dom F & ( for x being set st x in dom F holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
then consider f being Function such that
A8: dom f = dom F and
A9: for x being set st x in dom F holds
f . x = //\ ((F . x),L) ;
rng f c= the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of L )
assume y in rng f ; ::_thesis: y in the carrier of L
then consider x being set such that
A10: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
y = //\ ((F . x),L) by A8, A9, A10;
hence y in the carrier of L ; ::_thesis: verum
end;
then reconsider f = f as Function of (dom F), the carrier of L by A8, FUNCT_2:2;
take f ; ::_thesis: for x being set st x in dom F holds
f . x = //\ ((F . x),L)
thus for x being set st x in dom F holds
f . x = //\ ((F . x),L) by A9; ::_thesis: verum
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
let f, g be Function of (dom F), the carrier of L; ::_thesis: ( ( for x being set st x in dom F holds
f . x = //\ ((F . x),L) ) & ( for x being set st x in dom F holds
g . x = //\ ((F . x),L) ) implies f = g )
assume that
A11: for x being set st x in dom F holds
f . x = //\ ((F . x),L) and
A12: for x being set st x in dom F holds
g . x = //\ ((F . x),L) ; ::_thesis: f = g
A13: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom F implies f . x = g . x )
assume A14: x in dom F ; ::_thesis: f . x = g . x
hence f . x = //\ ((F . x),L) by A11
.= g . x by A12, A14 ;
::_thesis: verum
end;
( dom f = dom F & dom g = dom F ) by FUNCT_2:def_1;
hence f = g by A13, FUNCT_1:2; ::_thesis: verum
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
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
let L be non empty RelStr ; ::_thesis: 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)
let F, G be Function-yielding Function; ::_thesis: ( dom F = dom G & ( for x being set st x in dom F holds
\\/ ((F . x),L) = \\/ ((G . x),L) ) implies \// (F,L) = \// (G,L) )
assume that
A1: dom F = dom G and
A2: for x being set st x in dom F holds
\\/ ((F . x),L) = \\/ ((G . x),L) ; ::_thesis: \// (F,L) = \// (G,L)
A3: for x being set st x in dom F holds
(\// (F,L)) . x = (\// (G,L)) . x
proof
let x be set ; ::_thesis: ( x in dom F implies (\// (F,L)) . x = (\// (G,L)) . x )
assume A4: x in dom F ; ::_thesis: (\// (F,L)) . x = (\// (G,L)) . x
hence (\// (F,L)) . x = \\/ ((F . x),L) by Def1
.= \\/ ((G . x),L) by A2, A4
.= (\// (G,L)) . x by A1, A4, Def1 ;
::_thesis: verum
end;
( dom (\// (F,L)) = dom F & dom (\// (G,L)) = dom G ) by FUNCT_2:def_1;
hence \// (F,L) = \// (G,L) by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
theorem Th12: :: WAYBEL_5:12
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
let L be non empty RelStr ; ::_thesis: 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)
let F, G be Function-yielding Function; ::_thesis: ( dom F = dom G & ( for x being set st x in dom F holds
//\ ((F . x),L) = //\ ((G . x),L) ) implies /\\ (F,L) = /\\ (G,L) )
assume that
A1: dom F = dom G and
A2: for x being set st x in dom F holds
//\ ((F . x),L) = //\ ((G . x),L) ; ::_thesis: /\\ (F,L) = /\\ (G,L)
A3: for x being set st x in dom F holds
(/\\ (F,L)) . x = (/\\ (G,L)) . x
proof
let x be set ; ::_thesis: ( x in dom F implies (/\\ (F,L)) . x = (/\\ (G,L)) . x )
assume A4: x in dom F ; ::_thesis: (/\\ (F,L)) . x = (/\\ (G,L)) . x
hence (/\\ (F,L)) . x = //\ ((F . x),L) by Def2
.= //\ ((G . x),L) by A2, A4
.= (/\\ (G,L)) . x by A1, A4, Def2 ;
::_thesis: verum
end;
( dom (/\\ (F,L)) = dom F & dom (/\\ (G,L)) = dom G ) by FUNCT_2:def_1;
hence /\\ (F,L) = /\\ (G,L) by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
theorem Th13: :: WAYBEL_5:13
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
let y be set ; ::_thesis: 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)) ) )
let L be non empty RelStr ; ::_thesis: 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)) ) )
let F be Function-yielding Function; ::_thesis: ( ( 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)) ) )
thus ( y in rng (\// (F,L)) iff ex x being set st
( x in dom F & y = \\/ ((F . x),L) ) ) ::_thesis: ( y in rng (/\\ (F,L)) iff ex x being set st
( x in dom F & y = //\ ((F . x),L) ) )
proof
hereby ::_thesis: ( ex x being set st
( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) )
assume y in rng (\// (F,L)) ; ::_thesis: ex x being set st
( x in dom F & y = \\/ ((F . x),L) )
then consider x being set such that
A1: ( x in dom (\// (F,L)) & y = (\// (F,L)) . x ) by FUNCT_1:def_3;
take x = x; ::_thesis: ( x in dom F & y = \\/ ((F . x),L) )
thus ( x in dom F & y = \\/ ((F . x),L) ) by A1, Def1; ::_thesis: verum
end;
given x being set such that A2: ( x in dom F & y = \\/ ((F . x),L) ) ; ::_thesis: y in rng (\// (F,L))
( x in dom (\// (F,L)) & y = (\// (F,L)) . x ) by A2, Def1, FUNCT_2:def_1;
hence y in rng (\// (F,L)) by FUNCT_1:def_3; ::_thesis: verum
end;
thus ( y in rng (/\\ (F,L)) iff ex x being set st
( x in dom F & y = //\ ((F . x),L) ) ) ::_thesis: verum
proof
hereby ::_thesis: ( ex x being set st
( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) )
assume y in rng (/\\ (F,L)) ; ::_thesis: ex x being set st
( x in dom F & y = //\ ((F . x),L) )
then consider x being set such that
A3: ( x in dom (/\\ (F,L)) & y = (/\\ (F,L)) . x ) by FUNCT_1:def_3;
take x = x; ::_thesis: ( x in dom F & y = //\ ((F . x),L) )
thus ( x in dom F & y = //\ ((F . x),L) ) by A3, Def2; ::_thesis: verum
end;
given x being set such that A4: ( x in dom F & y = //\ ((F . x),L) ) ; ::_thesis: y in rng (/\\ (F,L))
( x in dom (/\\ (F,L)) & y = (/\\ (F,L)) . x ) by A4, Def2, FUNCT_2:def_1;
hence y in rng (/\\ (F,L)) by FUNCT_1:def_3; ::_thesis: verum
end;
end;
theorem Th14: :: WAYBEL_5:14
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
let x be set ; ::_thesis: 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 ) ) )
let L be non empty RelStr ; ::_thesis: 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 ) ) )
let J be non empty set ; ::_thesis: 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 ) ) )
let K be ManySortedSet of J; ::_thesis: 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 ) ) )
let F be DoubleIndexedSet of K,L; ::_thesis: ( ( 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 ) ) )
A1: dom F = J by PARTFUN1:def_2;
thus ( x in rng (Sups ) iff ex j being Element of J st x = Sup ) ::_thesis: ( x in rng (Infs ) iff ex j being Element of J st x = Inf )
proof
hereby ::_thesis: ( ex j being Element of J st x = Sup implies x in rng (Sups ) )
assume x in rng (Sups ) ; ::_thesis: ex j being Element of J st x = Sup
then consider j being set such that
A2: j in dom F and
A3: x = \\/ ((F . j),L) by Th13;
reconsider j = j as Element of J by A2;
take j = j; ::_thesis: x = Sup
thus x = Sup by A3; ::_thesis: verum
end;
thus ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) by A1, Th13; ::_thesis: verum
end;
hereby ::_thesis: ( ex j being Element of J st x = Inf implies x in rng (Infs ) )
assume x in rng (Infs ) ; ::_thesis: ex j being Element of J st x = Inf
then consider j being set such that
A4: j in dom F and
A5: x = //\ ((F . j),L) by Th13;
reconsider j = j as Element of J by A4;
take j = j; ::_thesis: x = Inf
thus x = Inf by A5; ::_thesis: verum
end;
thus ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) by A1, Th13; ::_thesis: verum
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 proj2 (Sups ) -> non empty ;
correctness
coherence
not rng (Sups ) is empty ;
;
cluster proj2 (Infs ) -> non empty ;
correctness
coherence
not rng (Infs ) is empty ;
;
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) )
proof
let L be complete LATTICE; ::_thesis: 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) )
let J be non empty set ; ::_thesis: 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) )
let K be V9() ManySortedSet of J; ::_thesis: 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) )
let F be DoubleIndexedSet of K,L; ::_thesis: for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )
let f be set ; ::_thesis: ( f is Element of product (doms F) iff f in dom (Frege F) )
hereby ::_thesis: ( f in dom (Frege F) implies f is Element of product (doms F) )
assume f is Element of product (doms F) ; ::_thesis: f in dom (Frege F)
then f in product (doms F) ;
hence f in dom (Frege F) by PARTFUN1:def_2; ::_thesis: verum
end;
thus ( f in dom (Frege F) implies f is Element of product (doms F) ) ; ::_thesis: verum
end;
theorem Th15: :: WAYBEL_5:15
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
let L be complete LATTICE; ::_thesis: 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
let a be Element of L; ::_thesis: 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
let F be Function-yielding Function; ::_thesis: ( ( for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ) implies Sup <= a )
assume A1: for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= a ; ::_thesis: Sup <= a
rng (/\\ ((Frege F),L)) is_<=_than a
proof
let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in rng (/\\ ((Frege F),L)) or c <= a )
assume c in rng (/\\ ((Frege F),L)) ; ::_thesis: c <= a
then consider f being set such that
A2: f in dom (Frege F) and
A3: c = //\ (((Frege F) . f),L) by Th13;
reconsider f = f as Function by A2;
f in dom (Frege F) by A2;
hence c <= a by A1, A3; ::_thesis: verum
end;
then sup (rng (/\\ ((Frege F),L))) <= a by YELLOW_0:32;
hence Sup <= a by YELLOW_2:def_5; ::_thesis: verum
end;
theorem Th16: :: WAYBEL_5:16
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 holds Inf >= Sup
proof
let L be complete LATTICE; ::_thesis: for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup
let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup
let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L holds Inf >= Sup
let F be DoubleIndexedSet of K,L; ::_thesis: Inf >= Sup
set a = Sup ;
A1: for j being Element of J
for f being Element of product (doms F) holds Sup >= Inf
proof
let j be Element of J; ::_thesis: for f being Element of product (doms F) holds Sup >= Inf
let f be Element of product (doms F); ::_thesis: Sup >= Inf
A2: f in dom (Frege F) by Lm7;
then reconsider k = f . j as Element of K . j by Lm6;
(F . j) . k = ((Frege F) . f) . j by A2, Lm5;
then A3: Inf <= (F . j) . k by YELLOW_2:53;
(F . j) . k <= Sup by YELLOW_2:53;
hence Sup >= Inf by A3, ORDERS_2:3; ::_thesis: verum
end;
Sup is_<=_than rng (Sups )
proof
let c be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not c in rng (Sups ) or Sup <= c )
assume c in rng (Sups ) ; ::_thesis: Sup <= c
then consider j being Element of J such that
A4: c = Sup by Th14;
for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= c by A1, A4;
hence Sup <= c by Th15; ::_thesis: verum
end;
then Sup <= inf (rng (Sups )) by YELLOW_0:33;
hence Inf >= Sup by YELLOW_2:def_6; ::_thesis: verum
end;
theorem Th17: :: WAYBEL_5:17
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
let L be complete LATTICE; ::_thesis: 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
let a, b be Element of L; ::_thesis: ( L is continuous & ( for c being Element of L st c << a holds
c <= b ) implies a <= b )
assume that
A1: L is continuous and
A2: for c being Element of L st c << a holds
c <= b ; ::_thesis: a <= b
now__::_thesis:_for_c_being_Element_of_L_st_c_in_waybelow_a_holds_
c_<=_b
let c be Element of L; ::_thesis: ( c in waybelow a implies c <= b )
assume c in waybelow a ; ::_thesis: c <= b
then c << a by WAYBEL_3:7;
hence c <= b by A2; ::_thesis: verum
end;
then waybelow a is_<=_than b by LATTICE3:def_9;
then sup (waybelow a) <= b by YELLOW_0:32;
hence a <= b by A1, WAYBEL_3:def_5; ::_thesis: verum
end;
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
proof
let L be complete LATTICE; ::_thesis: ( L is continuous implies 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 )
assume A1: L is continuous ; ::_thesis: 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
let J be non empty set ; ::_thesis: 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
let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A2: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup
now__::_thesis:_for_c_being_Element_of_L_st_c_<<_Inf_holds_
c_<=_Sup
let c be Element of L; ::_thesis: ( c << Inf implies c <= Sup )
assume A3: c << Inf ; ::_thesis: c <= Sup
A4: for j being Element of J holds c << Sup
proof
let j be Element of J; ::_thesis: c << Sup
Sup in rng (Sups ) by Th14;
then inf (rng (Sups )) <= Sup by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def_6;
hence c << Sup by A3, WAYBEL_3:2; ::_thesis: verum
end;
ex f being Function st
( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) )
proof
defpred S1[ set , set ] means ( $1 in J & $2 in K . $1 & ex b being Element of L st
( b = (F . $1) . $2 & c <= b ) );
A5: for j being Element of J ex k being Element of K . j st c <= (F . j) . k
proof
let j be Element of J; ::_thesis: ex k being Element of K . j st c <= (F . j) . k
A6: Sup <= sup (rng (F . j)) by YELLOW_2:def_5;
( rng (F . j) is non empty directed Subset of L & c << Sup ) by A2, A4;
then consider d being Element of L such that
A7: d in rng (F . j) and
A8: c <= d by A6, WAYBEL_3:def_1;
consider k being set such that
A9: k in dom (F . j) and
A10: d = (F . j) . k by A7, FUNCT_1:def_3;
reconsider k = k as Element of K . j by A9;
take k ; ::_thesis: c <= (F . j) . k
thus c <= (F . j) . k by A8, A10; ::_thesis: verum
end;
A11: for j being set st j in J holds
ex k being set st
( k in union (rng K) & S1[j,k] )
proof
let j be set ; ::_thesis: ( j in J implies ex k being set st
( k in union (rng K) & S1[j,k] ) )
assume j in J ; ::_thesis: ex k being set st
( k in union (rng K) & S1[j,k] )
then reconsider j9 = j as Element of J ;
consider k being Element of K . j9 such that
A12: c <= (F . j9) . k by A5;
take k ; ::_thesis: ( k in union (rng K) & S1[j,k] )
j9 in J ;
then j9 in dom K by PARTFUN1:def_2;
then K . j9 in rng K by FUNCT_1:def_3;
hence k in union (rng K) by TARSKI:def_4; ::_thesis: S1[j,k]
thus S1[j,k] by A12; ::_thesis: verum
end;
consider f being Function such that
A13: dom f = J and
rng f c= union (rng K) and
A14: for j being set st j in J holds
S1[j,f . j] from FUNCT_1:sch_5(A11);
A15: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_F)_holds_
f_._x_in_(doms_F)_._x
let x be set ; ::_thesis: ( x in dom (doms F) implies f . x in (doms F) . x )
assume x in dom (doms F) ; ::_thesis: f . x in (doms F) . x
then A16: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J ;
(doms F) . x = dom (F . j) by A16, FUNCT_6:22
.= K . j by FUNCT_2:def_1 ;
hence f . x in (doms F) . x by A14; ::_thesis: verum
end;
dom f = dom F by A13, PARTFUN1:def_2
.= dom (doms F) by FUNCT_6:59 ;
then f in product (doms F) by A15, CARD_3:9;
then A17: f in dom (Frege F) by PARTFUN1:def_2;
for j being Element of J holds
( f . j in K . j & ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) by A14;
hence ex f being Function st
( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) ) by A17; ::_thesis: verum
end;
then consider f being Function such that
A18: f in dom (Frege F) and
A19: for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ;
reconsider f = f as Element of product (doms F) by A18;
reconsider G = (Frege F) . f as Function of J, the carrier of L ;
now__::_thesis:_for_j_being_Element_of_J_holds_c_<=_G_._j
let j be Element of J; ::_thesis: c <= G . j
j in J ;
then A20: j in dom F by PARTFUN1:def_2;
ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) by A19;
hence c <= G . j by A18, A20, Th9; ::_thesis: verum
end;
then A21: c <= Inf by YELLOW_2:55;
set a = Inf ;
Inf in rng (Infs ) by Th14;
then Inf <= sup (rng (Infs )) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def_5;
hence c <= Sup by A21, YELLOW_0:def_2; ::_thesis: verum
end;
then A22: Inf <= Sup by A1, Th17;
Inf >= Sup by Th16;
hence Inf = Sup by A22, YELLOW_0:def_3; ::_thesis: verum
end;
theorem Th18: :: WAYBEL_5:18
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 V9() 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
let L be complete LATTICE; ::_thesis: ( ( for J being non empty set st J in the_universe_of the carrier of L holds
for K being V9() 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 ) implies L is continuous )
assume A1: for J being non empty set st J in the_universe_of the carrier of L holds
for K being V9() 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 ; ::_thesis: L is continuous
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x)
set UN = the_universe_of the carrier of L;
let x be Element of L; ::_thesis: x = sup (waybelow x)
set J = { j where j is non empty directed Subset of L : x <= sup j } ;
A2: the_universe_of the carrier of L = Tarski-Class (the_transitive-closure_of the carrier of L) by YELLOW_6:def_1;
reconsider UN = the_universe_of the carrier of L as universal set ;
A3: { j where j is non empty directed Subset of L : x <= sup j } c= bool the carrier of L
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { j where j is non empty directed Subset of L : x <= sup j } or u in bool the carrier of L )
assume u in { j where j is non empty directed Subset of L : x <= sup j } ; ::_thesis: u in bool the carrier of L
then ex j being non empty directed Subset of L st
( u = j & x <= sup j ) ;
hence u in bool the carrier of L ; ::_thesis: verum
end;
( the carrier of L c= the_transitive-closure_of the carrier of L & the_transitive-closure_of the carrier of L in UN ) by A2, CLASSES1:2, CLASSES1:52;
then A4: the carrier of L in UN by CLASSES1:def_1;
then bool the carrier of L in UN by CLASSES2:59;
then A5: { j where j is non empty directed Subset of L : x <= sup j } in UN by A3, CLASSES1:def_1;
x is_>=_than waybelow x by WAYBEL_3:9;
then A6: x >= sup (waybelow x) by YELLOW_0:32;
( {x} is non empty directed Subset of L & x <= sup {x} ) by WAYBEL_0:5, YELLOW_0:39;
then A7: {x} in { j where j is non empty directed Subset of L : x <= sup j } ;
then reconsider J = { j where j is non empty directed Subset of L : x <= sup j } as non empty set ;
set K = id J;
reconsider K = id J as ManySortedSet of J ;
A8: for j being Element of J holds K . j in UN
proof
let j be Element of J; ::_thesis: K . j in UN
K . j = j by FUNCT_1:18;
then K . j in J ;
hence K . j in UN by A4, A3, CLASSES1:def_1; ::_thesis: verum
end;
reconsider j = {x} as Element of J by A7;
A9: for j being Element of J holds j is non empty directed Subset of L
proof
let j be Element of J; ::_thesis: j is non empty directed Subset of L
j in J ;
then ex j9 being non empty directed Subset of L st
( j9 = j & x <= sup j9 ) ;
hence j is non empty directed Subset of L ; ::_thesis: verum
end;
for i being set st i in J holds
not K . i is empty
proof
let i be set ; ::_thesis: ( i in J implies not K . i is empty )
assume i in J ; ::_thesis: not K . i is empty
then reconsider i9 = i as Element of J ;
K . i = i9 by FUNCT_1:18;
hence not K . i is empty by A9; ::_thesis: verum
end;
then reconsider K = K as V9() ManySortedSet of J by PBOOLE:def_13;
deffunc H1( set ) -> Element of bool [:(K . $1),(K . $1):] = id (K . $1);
ex F being Function st
( dom F = J & ( for j being set st j in J holds
F . j = H1(j) ) ) from FUNCT_1:sch_3();
then consider F being Function such that
A10: dom F = J and
A11: for j being set st j in J holds
F . j = id (K . j) ;
reconsider F = F as ManySortedSet of J by A10, PARTFUN1:def_2, RELAT_1:def_18;
for j being set st j in dom F holds
F . j is Function
proof
let j be set ; ::_thesis: ( j in dom F implies F . j is Function )
assume j in dom F ; ::_thesis: F . j is Function
then F . j = id (K . j) by A11;
hence F . j is Function ; ::_thesis: verum
end;
then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def_6;
for j being set st j in J holds
F . j is Function of (K . j),((J --> the carrier of L) . j)
proof
let j be set ; ::_thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) )
assume j in J ; ::_thesis: F . j is Function of (K . j),((J --> the carrier of L) . j)
then reconsider j = j as Element of J ;
K . j = j by FUNCT_1:18;
then A12: K . j is Subset of L by A9;
A13: F . j = id (K . j) by A11;
then rng (F . j) c= K . j by RELAT_1:def_19;
then rng (F . j) c= the carrier of L by A12, XBOOLE_1:1;
then A14: rng (F . j) c= (J --> the carrier of L) . j by FUNCOP_1:7;
dom (F . j) = K . j by A13, FUNCT_2:def_1;
hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A14, FUNCT_2:2; ::_thesis: verum
end;
then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def_15;
A15: for j being Element of J
for k being Element of K . j holds (F . j) . k = k
proof
let j be Element of J; ::_thesis: for k being Element of K . j holds (F . j) . k = k
let k be Element of K . j; ::_thesis: (F . j) . k = k
F . j = id (K . j) by A11;
hence (F . j) . k = k by FUNCT_1:18; ::_thesis: verum
end;
A16: for j being Element of J holds rng (F . j) = j
proof
let j be Element of J; ::_thesis: rng (F . j) = j
now__::_thesis:_for_y_being_set_st_y_in_rng_(F_._j)_holds_
y_in_j
let y be set ; ::_thesis: ( y in rng (F . j) implies y in j )
assume y in rng (F . j) ; ::_thesis: y in j
then consider x being set such that
A17: x in dom (F . j) and
A18: y = (F . j) . x by FUNCT_1:def_3;
x in K . j by A17;
then x in j by FUNCT_1:18;
hence y in j by A15, A17, A18; ::_thesis: verum
end;
then A19: rng (F . j) c= j by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_j_holds_
x_in_rng_(F_._j)
let x be set ; ::_thesis: ( x in j implies x in rng (F . j) )
assume x in j ; ::_thesis: x in rng (F . j)
then x in K . j by FUNCT_1:18;
then ( (F . j) . x = x & x in dom (F . j) ) by A15, FUNCT_2:def_1;
hence x in rng (F . j) by FUNCT_1:def_3; ::_thesis: verum
end;
then j c= rng (F . j) by TARSKI:def_3;
hence rng (F . j) = j by A19, XBOOLE_0:def_10; ::_thesis: verum
end;
A20: for j being Element of J holds rng (F . j) is directed
proof
let j be Element of J; ::_thesis: rng (F . j) is directed
rng (F . j) = j by A16;
hence rng (F . j) is directed by A9; ::_thesis: verum
end;
for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= sup (waybelow x)
proof
let f be Function; ::_thesis: ( f in dom (Frege F) implies //\ (((Frege F) . f),L) <= sup (waybelow x) )
assume A21: f in dom (Frege F) ; ::_thesis: //\ (((Frege F) . f),L) <= sup (waybelow x)
set a = //\ (((Frege F) . f),L);
for D being non empty directed Subset of L st x <= sup D holds
ex d being Element of L st
( d in D & //\ (((Frege F) . f),L) <= d )
proof
A22: for j being Element of J holds f . j in K . j
proof
let j be Element of J; ::_thesis: f . j in K . j
j in J ;
then j in dom F by PARTFUN1:def_2;
then f . j in dom (F . j) by A21, Th9;
hence f . j in K . j ; ::_thesis: verum
end;
A23: dom f = dom F by A21, Th8
.= J by PARTFUN1:def_2 ;
now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_
y_in_the_carrier_of_L
let y be set ; ::_thesis: ( y in rng f implies y in the carrier of L )
assume y in rng f ; ::_thesis: y in the carrier of L
then consider j being set such that
A24: j in dom f and
A25: y = f . j by FUNCT_1:def_3;
reconsider j = j as Element of J by A23, A24;
y in K . j by A22, A25;
then A26: y in j by FUNCT_1:18;
j is Subset of L by A9;
hence y in the carrier of L by A26; ::_thesis: verum
end;
then rng f c= the carrier of L by TARSKI:def_3;
then reconsider f = f as Function of J, the carrier of L by A23, FUNCT_2:2;
let D be non empty directed Subset of L; ::_thesis: ( x <= sup D implies ex d being Element of L st
( d in D & //\ (((Frege F) . f),L) <= d ) )
assume x <= sup D ; ::_thesis: ex d being Element of L st
( d in D & //\ (((Frege F) . f),L) <= d )
then D in J ;
then reconsider D9 = D as Element of J ;
A27: Inf <= f . D9 by YELLOW_2:53;
f . D9 in K . D9 by A22;
then A28: f . D9 in D9 by FUNCT_1:18;
A29: now__::_thesis:_for_j_being_set_st_j_in_dom_f_holds_
((Frege_F)_._f)_._j_=_f_._j
let j be set ; ::_thesis: ( j in dom f implies ((Frege F) . f) . j = f . j )
assume A30: j in dom f ; ::_thesis: ((Frege F) . f) . j = f . j
then reconsider j9 = j as Element of J ;
A31: f . j9 is Element of K . j9 by A22;
j in dom F by A21, A30, Th8;
hence ((Frege F) . f) . j = (F . j9) . (f . j9) by A21, Th9
.= f . j by A15, A31 ;
::_thesis: verum
end;
dom f = dom F by A21, Th8
.= dom ((Frege F) . f) by A21, Th8 ;
then //\ (((Frege F) . f),L) <= f . D9 by A27, A29, FUNCT_1:2;
hence ex d being Element of L st
( d in D & //\ (((Frege F) . f),L) <= d ) by A28; ::_thesis: verum
end;
then //\ (((Frege F) . f),L) << x by WAYBEL_3:def_1;
then //\ (((Frege F) . f),L) in waybelow x by WAYBEL_3:7;
hence //\ (((Frege F) . f),L) <= sup (waybelow x) by YELLOW_2:22; ::_thesis: verum
end;
then A32: Sup <= sup (waybelow x) by Th15;
x is_<=_than rng (Sups )
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in rng (Sups ) or x <= b )
assume b in rng (Sups ) ; ::_thesis: x <= b
then consider j being Element of J such that
A33: b = Sup by Th14;
j in J ;
then consider j9 being non empty directed Subset of L such that
A34: j9 = j and
A35: x <= sup j9 ;
b = sup (rng (F . j)) by A33, YELLOW_2:def_5
.= sup j9 by A16, A34 ;
hence x <= b by A35; ::_thesis: verum
end;
then x <= inf (rng (Sups )) by YELLOW_0:33;
then A36: x <= Inf by YELLOW_2:def_6;
Sup = sup (rng (F . j)) by YELLOW_2:def_5
.= sup {x} by A16
.= x by YELLOW_0:39 ;
then x in rng (Sups ) by Th14;
then inf (rng (Sups )) <= x by YELLOW_2:22;
then Inf <= x by YELLOW_2:def_6;
then x = Inf by A36, ORDERS_2:2
.= Sup by A1, A5, A8, A20 ;
hence x = sup (waybelow x) by A32, A6, ORDERS_2:2; ::_thesis: verum
end;
then ( L is up-complete & L is satisfying_axiom_of_approximation ) by WAYBEL_3:def_5;
hence L is continuous ; ::_thesis: verum
end;
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
proof
let L be complete LATTICE; ::_thesis: ( ( 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 ) implies L is continuous )
assume 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 ; ::_thesis: L is continuous
then for J being non empty set st J in the_universe_of the carrier of L holds
for K being V9() 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 ;
hence L is continuous by Th18; ::_thesis: verum
end;
theorem :: WAYBEL_5:19
for L being complete LATTICE holds
( L is continuous iff 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 ) 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
reconsider F9 = F as ManySortedSet of [:J,K:] ;
A1: dom F = [:J,K:] by FUNCT_2:def_1;
for j being set st j in J holds
(curry F9) . j is Function of ((J --> K) . j),((J --> D) . j)
proof
let j be set ; ::_thesis: ( j in J implies (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) )
assume A2: j in J ; ::_thesis: (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j)
then consider g being Function such that
A3: (curry F9) . j = g and
A4: dom g = K and
A5: rng g c= rng F9 and
for k being set st k in K holds
g . k = F9 . (j,k) by A1, FUNCT_5:29;
J = dom (curry F) by A1, FUNCT_5:24;
then reconsider G = (curry F9) . j as Function ;
rng F c= D ;
then rng g c= D by A5, XBOOLE_1:1;
then reconsider g = g as Function of K,D by A4, FUNCT_2:def_1, RELSET_1:4;
A6: G = g by A3;
(J --> K) . j = K by A2, FUNCOP_1:7;
hence (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) by A2, A6, FUNCOP_1:7; ::_thesis: verum
end;
hence curry F is DoubleIndexedSet of J --> K,D by PBOOLE:def_15; ::_thesis: verum
end;
end;
theorem Th20: :: WAYBEL_5:20
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
let J, K, D be non empty set ; ::_thesis: 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 )
let j be Element of J; ::_thesis: 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 )
let k be Element of K; ::_thesis: 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 )
let F be Function of [:J,K:],D; ::_thesis: ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k )
thus dom (curry F) = proj1 (dom F) by FUNCT_5:def_1
.= proj1 [:J,K:] by FUNCT_2:def_1
.= J by FUNCT_5:9 ; ::_thesis: ( dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k )
dom F = [:J,K:] by FUNCT_2:def_1;
then ex g being Function st
( (curry F) . j = g & dom g = K & rng g c= rng F & ( for i being set st i in K holds
g . i = F . (j,i) ) ) by FUNCT_5:29;
hence dom ((curry F) . j) = K ; ::_thesis: F . (j,k) = ((curry F) . j) . k
[j,k] in [:J,K:] ;
then [j,k] in dom F by FUNCT_2:def_1;
hence F . (j,k) = ((curry F) . j) . k by FUNCT_5:20; ::_thesis: verum
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
let L be complete LATTICE; ::_thesis: ( ( 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 ) implies L is continuous )
assume A1: 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 ; ::_thesis: L is continuous
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
proof
let J be non empty set ; ::_thesis: 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
let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
set j = the Element of J;
set k = the Element of K . the Element of J;
defpred S1[ set , set , set ] means ( $1 in J & ( ( $2 in K . $1 & $3 = (F . $1) . $2 ) or ( not $2 in K . $1 & $3 = Bottom L ) ) );
A2: dom (doms F) = dom F by FUNCT_6:59;
the Element of J in J ;
then the Element of J in dom K by PARTFUN1:def_2;
then ( the Element of K . the Element of J in K . the Element of J & K . the Element of J in rng K ) by FUNCT_1:def_3;
then reconsider K9 = union (rng K) as non empty set by TARSKI:def_4;
A3: dom F = J by PARTFUN1:def_2;
A4: for j being Element of J
for k9 being Element of K9 ex z being Element of L st S1[j,k9,z]
proof
let j be Element of J; ::_thesis: for k9 being Element of K9 ex z being Element of L st S1[j,k9,z]
let k9 be Element of K9; ::_thesis: ex z being Element of L st S1[j,k9,z]
percases ( k9 in K . j or not k9 in K . j ) ;
suppose k9 in K . j ; ::_thesis: ex z being Element of L st S1[j,k9,z]
then reconsider k = k9 as Element of K . j ;
take (F . j) . k ; ::_thesis: S1[j,k9,(F . j) . k]
thus S1[j,k9,(F . j) . k] ; ::_thesis: verum
end;
supposeA5: not k9 in K . j ; ::_thesis: ex z being Element of L st S1[j,k9,z]
take Bottom L ; ::_thesis: S1[j,k9, Bottom L]
thus S1[j,k9, Bottom L] by A5; ::_thesis: verum
end;
end;
end;
ex G being Function of [:J,K9:], the carrier of L st
for j being Element of J
for k being Element of K9 holds S1[j,k,G . (j,k)] from BINOP_1:sch_3(A4);
then consider G being Function of [:J,K9:], the carrier of L such that
A6: for j being Element of J
for k being Element of K9 holds S1[j,k,G . (j,k)] ;
A7: for j being Element of J holds K . j c= K9
proof
let j be Element of J; ::_thesis: K . j c= K9
hereby :: according to TARSKI:def_3 ::_thesis: verum
let k be set ; ::_thesis: ( k in K . j implies k in K9 )
j in J ;
then j in dom K by PARTFUN1:def_2;
then A8: K . j in rng K by FUNCT_1:def_3;
assume k in K . j ; ::_thesis: k in K9
hence k in K9 by A8, TARSKI:def_4; ::_thesis: verum
end;
end;
A9: for j being Element of J holds rng (F . j) c= rng ((curry G) . j)
proof
let j be Element of J; ::_thesis: rng (F . j) c= rng ((curry G) . j)
hereby :: according to TARSKI:def_3 ::_thesis: verum
let y be set ; ::_thesis: ( y in rng (F . j) implies y in rng ((curry G) . j) )
assume y in rng (F . j) ; ::_thesis: y in rng ((curry G) . j)
then consider k being set such that
A10: k in dom (F . j) and
A11: y = (F . j) . k by FUNCT_1:def_3;
A12: k in K . j by A10;
K . j c= K9 by A7;
then reconsider k = k as Element of K9 by A12;
[j,k] in [:J,K9:] ;
then A13: [j,k] in dom G by FUNCT_2:def_1;
( k in K9 & dom ((curry G) . j) = (J --> K9) . j ) by FUNCT_2:def_1;
then A14: k in dom ((curry G) . j) by FUNCOP_1:7;
y = G . (j,k) by A6, A10, A11
.= ((curry G) . j) . k by A13, FUNCT_5:20 ;
hence y in rng ((curry G) . j) by A14, FUNCT_1:def_3; ::_thesis: verum
end;
end;
A15: for j being set st j in dom F holds
\\/ ((F . j),L) = \\/ (((curry G) . j),L)
proof
let j9 be set ; ::_thesis: ( j9 in dom F implies \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) )
assume j9 in dom F ; ::_thesis: \\/ ((F . j9),L) = \\/ (((curry G) . j9),L)
then reconsider j = j9 as Element of J ;
reconsider H = (curry G) . j as Function of ((J --> K9) . j), the carrier of L ;
(J --> K9) . j = K9 by FUNCOP_1:7;
then reconsider H = H as Function of K9, the carrier of L ;
for k being Element of K9 holds H . k <= Sup
proof
let k be Element of K9; ::_thesis: H . k <= Sup
percases ( k in K . j or not k in K . j ) ;
supposeA16: k in K . j ; ::_thesis: H . k <= Sup
then A17: k in dom (F . j) by FUNCT_2:def_1;
(F . j) . k = G . (j,k) by A6, A16
.= H . k by Th20 ;
then H . k in rng (F . j) by A17, FUNCT_1:def_3;
then H . k <= sup (rng (F . j)) by YELLOW_2:22;
hence H . k <= Sup by YELLOW_2:def_5; ::_thesis: verum
end;
suppose not k in K . j ; ::_thesis: H . k <= Sup
then Bottom L = G . (j,k) by A6
.= H . k by Th20 ;
hence H . k <= Sup by YELLOW_0:44; ::_thesis: verum
end;
end;
end;
then A18: Sup <= Sup by YELLOW_2:54;
( ex_sup_of rng (F . j),L & ex_sup_of rng ((curry G) . j),L ) by YELLOW_0:17;
then sup (rng (F . j)) <= sup (rng ((curry G) . j)) by A9, YELLOW_0:34;
then Sup <= sup (rng H) by YELLOW_2:def_5;
then Sup <= Sup by YELLOW_2:def_5;
hence \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) by A18, ORDERS_2:2; ::_thesis: verum
end;
A19: dom (doms (curry G)) = dom (curry G) by FUNCT_6:59;
A20: dom (curry G) = J by Th20;
product (doms F) c= product (doms (curry G))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (doms F) or x in product (doms (curry G)) )
assume x in product (doms F) ; ::_thesis: x in product (doms (curry G))
then consider g being Function such that
A21: x = g and
A22: dom g = dom (doms F) and
A23: for j being set st j in dom (doms F) holds
g . j in (doms F) . j by CARD_3:def_5;
A24: for j being set st j in dom (doms (curry G)) holds
g . j in (doms (curry G)) . j
proof
let j be set ; ::_thesis: ( j in dom (doms (curry G)) implies g . j in (doms (curry G)) . j )
assume A25: j in dom (doms (curry G)) ; ::_thesis: g . j in (doms (curry G)) . j
then reconsider j9 = j as Element of J by A19;
j in J by A19, A25;
then A26: g . j in (doms F) . j by A2, A3, A23;
A27: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22
.= K . j9 by FUNCT_2:def_1 ;
A28: K . j9 c= K9 by A7;
(doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22
.= K9 by Th20 ;
hence g . j in (doms (curry G)) . j by A26, A27, A28; ::_thesis: verum
end;
dom g = dom (doms (curry G)) by A2, A3, A19, A22, Th20;
hence x in product (doms (curry G)) by A21, A24, CARD_3:def_5; ::_thesis: verum
end;
then dom (Frege F) c= product (doms (curry G)) by PARTFUN1:def_2;
then A29: dom (Frege F) c= dom (Frege (curry G)) by PARTFUN1:def_2;
A30: for f being set st f in dom (Frege F) holds
//\ (((Frege F) . f),L) = //\ (((Frege (curry G)) . f),L)
proof
let f9 be set ; ::_thesis: ( f9 in dom (Frege F) implies //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) )
assume A31: f9 in dom (Frege F) ; ::_thesis: //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L)
then reconsider f = f9 as Element of product (doms F) ;
A32: dom ((Frege F) . f) = dom F by A31, Th8
.= J by PARTFUN1:def_2 ;
A33: for j being set st j in J holds
((Frege F) . f) . j = ((Frege (curry G)) . f) . j
proof
let j9 be set ; ::_thesis: ( j9 in J implies ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 )
assume j9 in J ; ::_thesis: ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9
then reconsider j = j9 as Element of J ;
A34: f . j in K . j by A31, Lm6;
K . j c= K9 by A7;
then reconsider fj = f . j as Element of K9 by A34;
((Frege F) . f) . j = (F . j) . fj by A31, Lm5
.= G . (j,fj) by A6, A34
.= ((curry G) . j) . (f . j) by Th20
.= ((Frege (curry G)) . f) . j by A29, A31, Lm5 ;
hence ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 ; ::_thesis: verum
end;
dom ((Frege (curry G)) . f) = dom (curry G) by A29, A31, Th8
.= proj1 (dom G) by FUNCT_5:def_1
.= proj1 [:J,K9:] by FUNCT_2:def_1
.= J by FUNCT_5:9 ;
hence //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) by A32, A33, FUNCT_1:2; ::_thesis: verum
end;
A35: Sup = Sup
proof
percases ( for j being Element of J holds K . j = K9 or ex j being Element of J st K . j <> K9 ) ;
supposeA36: for j being Element of J holds K . j = K9 ; ::_thesis: Sup = Sup
for j being set st j in J holds
(doms F) . j = (doms (curry G)) . j
proof
let j be set ; ::_thesis: ( j in J implies (doms F) . j = (doms (curry G)) . j )
assume j in J ; ::_thesis: (doms F) . j = (doms (curry G)) . j
then reconsider j9 = j as Element of J ;
A37: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22
.= K . j9 by FUNCT_2:def_1 ;
(doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22
.= K9 by Th20 ;
hence (doms F) . j = (doms (curry G)) . j by A36, A37; ::_thesis: verum
end;
then doms F = doms (curry G) by A2, A3, A19, A20, FUNCT_1:2;
then dom (Frege F) = product (doms (curry G)) by PARTFUN1:def_2;
then dom (Frege F) = dom (Frege (curry G)) by PARTFUN1:def_2;
hence Sup = Sup by A30, Th12; ::_thesis: verum
end;
suppose ex j being Element of J st K . j <> K9 ; ::_thesis: Sup = Sup
then consider j being Element of J such that
A38: K . j <> K9 ;
K . j c= K9 by A7;
then not K9 c= K . j by A38, XBOOLE_0:def_10;
then consider k being set such that
A39: k in K9 and
A40: not k in K . j by TARSKI:def_3;
reconsider k = k as Element of K9 by A39;
A41: (rng (Infs )) \/ {(Bottom L)} c= rng (Infs )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng (Infs )) \/ {(Bottom L)} or x in rng (Infs ) )
assume A42: x in (rng (Infs )) \/ {(Bottom L)} ; ::_thesis: x in rng (Infs )
percases ( x in rng (Infs ) or x in {(Bottom L)} ) by A42, XBOOLE_0:def_3;
suppose x in rng (Infs ) ; ::_thesis: x in rng (Infs )
then consider f being set such that
A43: f in dom (Frege F) and
A44: x = //\ (((Frege F) . f),L) by Th13;
x = //\ (((Frege (curry G)) . f),L) by A30, A43, A44;
hence x in rng (Infs ) by A29, A43, Th13; ::_thesis: verum
end;
supposeA45: x in {(Bottom L)} ; ::_thesis: x in rng (Infs )
then reconsider x9 = x as Element of L ;
set f = J --> k;
A46: for x being set st x in dom (doms (curry G)) holds
(J --> k) . x in (doms (curry G)) . x
proof
let x be set ; ::_thesis: ( x in dom (doms (curry G)) implies (J --> k) . x in (doms (curry G)) . x )
assume x in dom (doms (curry G)) ; ::_thesis: (J --> k) . x in (doms (curry G)) . x
then reconsider j = x as Element of J by A19;
A47: (J --> k) . j = k by FUNCOP_1:7;
(doms (curry G)) . j = dom ((curry G) . j) by A20, FUNCT_6:22
.= K9 by Th20 ;
hence (J --> k) . x in (doms (curry G)) . x by A47; ::_thesis: verum
end;
dom (J --> k) = J by FUNCOP_1:13
.= dom (doms (curry G)) by A19, Th20 ;
then J --> k in product (doms (curry G)) by A46, CARD_3:9;
then A48: J --> k in dom (Frege (curry G)) by PARTFUN1:def_2;
A49: x = Bottom L by A45, TARSKI:def_1;
then x = G . (j,k) by A6, A40
.= ((curry G) . j) . k by Th20
.= ((curry G) . j) . ((J --> k) . j) by FUNCOP_1:7 ;
then x in rng ((Frege (curry G)) . (J --> k)) by A48, Lm5;
then x9 >= "/\" ((rng ((Frege (curry G)) . (J --> k))),L) by YELLOW_2:22;
then A50: x9 >= //\ (((Frege (curry G)) . (J --> k)),L) by YELLOW_2:def_6;
x9 <= //\ (((Frege (curry G)) . (J --> k)),L) by A49, YELLOW_0:44;
then x9 = //\ (((Frege (curry G)) . (J --> k)),L) by A50, ORDERS_2:2;
hence x in rng (Infs ) by A48, Th13; ::_thesis: verum
end;
end;
end;
A51: ( ex_sup_of rng (Infs ),L & ex_sup_of {(Bottom L)},L ) by YELLOW_0:17;
A52: rng (Infs ) c= (rng (Infs )) \/ {(Bottom L)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Infs ) or x in (rng (Infs )) \/ {(Bottom L)} )
assume x in rng (Infs ) ; ::_thesis: x in (rng (Infs )) \/ {(Bottom L)}
then consider f being set such that
A53: f in dom (Frege (curry G)) and
A54: x = //\ (((Frege (curry G)) . f),L) by Th13;
reconsider f = f as Function by A53;
percases ( for j being Element of J holds f . j in K . j or ex j being Element of J st not f . j in K . j ) ;
supposeA55: for j being Element of J holds f . j in K . j ; ::_thesis: x in (rng (Infs )) \/ {(Bottom L)}
A56: for x being set st x in dom (doms F) holds
f . x in (doms F) . x
proof
let x be set ; ::_thesis: ( x in dom (doms F) implies f . x in (doms F) . x )
assume x in dom (doms F) ; ::_thesis: f . x in (doms F) . x
then reconsider j = x as Element of J by A3, FUNCT_6:59;
(doms F) . j = dom (F . j) by A3, FUNCT_6:22
.= K . j by FUNCT_2:def_1 ;
hence f . x in (doms F) . x by A55; ::_thesis: verum
end;
dom f = dom (curry G) by A53, Th8
.= dom (doms F) by A2, A3, Th20 ;
then f in product (doms F) by A56, CARD_3:9;
then A57: f in dom (Frege F) by PARTFUN1:def_2;
then x = //\ (((Frege F) . f),L) by A30, A54;
then x in rng (Infs ) by A57, Th13;
hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not for j being Element of J holds f . j in K . j ; ::_thesis: x in (rng (Infs )) \/ {(Bottom L)}
then consider j being Element of J such that
A58: not f . j in K . j ;
j in J ;
then j in dom (curry G) by Th20;
then f . j in dom ((curry G) . j) by A53, Th9;
then reconsider k = f . j as Element of K9 by Th20;
Bottom L = G . (j,k) by A6, A58
.= ((curry G) . j) . (f . j) by Th20 ;
then Bottom L in rng ((Frege (curry G)) . f) by A53, Lm5;
then Bottom L >= "/\" ((rng ((Frege (curry G)) . f)),L) by YELLOW_2:22;
then A59: Bottom L >= //\ (((Frege (curry G)) . f),L) by YELLOW_2:def_6;
Bottom L <= //\ (((Frege (curry G)) . f),L) by YELLOW_0:44;
then x = Bottom L by A54, A59, ORDERS_2:2;
then x in {(Bottom L)} by TARSKI:def_1;
hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
A60: Bottom L <= Sup by YELLOW_0:44;
Sup = sup (rng (Infs )) by YELLOW_2:def_5
.= sup ((rng (Infs )) \/ {(Bottom L)}) by A52, A41, XBOOLE_0:def_10
.= (sup (rng (Infs ))) "\/" (sup {(Bottom L)}) by A51, YELLOW_2:3
.= (sup (rng (Infs ))) "\/" (Bottom L) by YELLOW_0:39
.= (Sup ) "\/" (Bottom L) by YELLOW_2:def_5
.= Sup by A60, YELLOW_0:24 ;
hence Sup = Sup ; ::_thesis: verum
end;
end;
end;
assume A61: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup
A62: for j being Element of J holds rng ((curry G) . j) is directed
proof
let j be Element of J; ::_thesis: rng ((curry G) . j) is directed
set X = rng ((curry G) . j);
for x, y being Element of L st x in rng ((curry G) . j) & y in rng ((curry G) . j) holds
ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z )
proof
A63: rng (F . j) is directed by A61;
let x, y be Element of L; ::_thesis: ( x in rng ((curry G) . j) & y in rng ((curry G) . j) implies ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z ) )
assume that
A64: x in rng ((curry G) . j) and
A65: y in rng ((curry G) . j) ; ::_thesis: ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z )
consider b being set such that
A66: b in dom ((curry G) . j) and
A67: ((curry G) . j) . b = y by A65, FUNCT_1:def_3;
consider a being set such that
A68: a in dom ((curry G) . j) and
A69: ((curry G) . j) . a = x by A64, FUNCT_1:def_3;
reconsider a9 = a, b9 = b as Element of K9 by A68, A66, Th20;
A70: x = G . (j,a9) by A69, Th20;
A71: y = G . (j,b9) by A67, Th20;
percases ( ( a in K . j & b in K . j ) or ( a in K . j & not b in K . j ) or ( not a in K . j & b in K . j ) or ( not a in K . j & not b in K . j ) ) ;
supposeA72: ( a in K . j & b in K . j ) ; ::_thesis: ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z )
then ( b in dom (F . j) & y = (F . j) . b9 ) by A6, A71, FUNCT_2:def_1;
then A73: y in rng (F . j) by FUNCT_1:def_3;
( a in dom (F . j) & x = (F . j) . a9 ) by A6, A70, A72, FUNCT_2:def_1;
then x in rng (F . j) by FUNCT_1:def_3;
then consider z being Element of L such that
A74: ( z in rng (F . j) & x <= z & y <= z ) by A63, A73, WAYBEL_0:def_1;
take z ; ::_thesis: ( z in rng ((curry G) . j) & x <= z & y <= z )
rng (F . j) c= rng ((curry G) . j) by A9;
hence ( z in rng ((curry G) . j) & x <= z & y <= z ) by A74; ::_thesis: verum
end;
supposeA75: ( a in K . j & not b in K . j ) ; ::_thesis: ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z )
take x ; ::_thesis: ( x in rng ((curry G) . j) & x <= x & y <= x )
y = Bottom L by A6, A71, A75;
hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A64, YELLOW_0:44; ::_thesis: verum
end;
supposeA76: ( not a in K . j & b in K . j ) ; ::_thesis: ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z )
take y ; ::_thesis: ( y in rng ((curry G) . j) & x <= y & y <= y )
x = Bottom L by A6, A70, A76;
hence ( y in rng ((curry G) . j) & x <= y & y <= y ) by A65, YELLOW_0:44; ::_thesis: verum
end;
supposeA77: ( not a in K . j & not b in K . j ) ; ::_thesis: ex z being Element of L st
( z in rng ((curry G) . j) & x <= z & y <= z )
take x ; ::_thesis: ( x in rng ((curry G) . j) & x <= x & y <= x )
x = Bottom L by A6, A70, A77;
hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A6, A64, A71, A77; ::_thesis: verum
end;
end;
end;
hence rng ((curry G) . j) is directed by WAYBEL_0:def_1; ::_thesis: verum
end;
dom F = J by PARTFUN1:def_2
.= dom (curry G) by PARTFUN1:def_2 ;
hence Inf = Inf by A15, Th11
.= Sup by A1, A62, A35 ;
::_thesis: verum
end;
hence L is continuous by Lm9; ::_thesis: verum
end;
theorem :: WAYBEL_5:21
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
let J, K be non empty set ; ::_thesis: 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
let f be Function; ::_thesis: ( f in Funcs (J,(Fin K)) implies for j being Element of J holds f . j is finite Subset of K )
assume f in Funcs (J,(Fin K)) ; ::_thesis: for j being Element of J holds f . j is finite Subset of K
then A1: ex f9 being Function st
( f9 = f & dom f9 = J & rng f9 c= Fin K ) by FUNCT_2:def_2;
for j being Element of J holds f . j is finite Subset of K
proof
let j be Element of J; ::_thesis: f . j is finite Subset of K
f . j in rng f by A1, FUNCT_1:def_3;
hence f . j is finite Subset of K by A1, FINSUB_1:def_5; ::_thesis: verum
end;
hence for j being Element of J holds f . j is finite Subset of K ; ::_thesis: verum
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 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 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
let L be complete LATTICE; ::_thesis: 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 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))
let J, K, D be non empty set ; ::_thesis: 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 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))
let j be Element of J; ::_thesis: 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 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))
let F be Function of [:J,K:],D; ::_thesis: 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 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))
let f be V9() ManySortedSet of J; ::_thesis: ( f in Funcs (J,(Fin K)) implies 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)) )
assume f in Funcs (J,(Fin K)) ; ::_thesis: 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))
then A1: f . j is finite Subset of K by Lm11;
let G be DoubleIndexedSet of f,L; ::_thesis: ( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) ) implies rng (G . j) is finite Subset of (rng ((curry F) . j)) )
assume A2: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) ; ::_thesis: rng (G . j) is finite Subset of (rng ((curry F) . j))
rng (G . j) c= rng ((curry F) . j)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (G . j) or y in rng ((curry F) . j) )
assume y in rng (G . j) ; ::_thesis: y in rng ((curry F) . j)
then consider k being set such that
A3: k in dom (G . j) and
A4: y = (G . j) . k by FUNCT_1:def_3;
A5: k in f . j by A3;
then A6: k in K by A1;
reconsider k = k as Element of K by A1, A5;
A7: k in dom ((curry F) . j) by A6, Th20;
y = F . (j,k) by A2, A3, A4
.= ((curry F) . j) . k by Th20 ;
hence y in rng ((curry F) . j) by A7, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng (G . j) is finite Subset of (rng ((curry F) . j)) by A1; ::_thesis: verum
end;
theorem Th22: :: WAYBEL_5:22
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 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf >= sup X
proof
let L be complete LATTICE; ::_thesis: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf >= sup X
let J, K be non empty set ; ::_thesis: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf >= sup X
let F be Function of [:J,K:], the carrier of L; ::_thesis: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf >= sup X
let X be Subset of L; ::_thesis: ( 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } implies Inf >= sup X )
A1: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) holds
for j being Element of J holds Sup >= Sup
proof
let f be V9() ManySortedSet of J; ::_thesis: ( f in Funcs (J,(Fin K)) implies 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
for j being Element of J holds Sup >= Sup )
assume A2: f in Funcs (J,(Fin K)) ; ::_thesis: 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
for j being Element of J holds Sup >= Sup
let G be DoubleIndexedSet of f,L; ::_thesis: ( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) ) implies for j being Element of J holds Sup >= Sup )
assume A3: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) ; ::_thesis: for j being Element of J holds Sup >= Sup
let j be Element of J; ::_thesis: Sup >= Sup
A4: ( ex_sup_of rng ((curry F) . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;
rng (G . j) is Subset of (rng ((curry F) . j)) by A2, A3, Lm12;
then sup (rng ((curry F) . j)) >= sup (rng (G . j)) by A4, YELLOW_0:34;
then Sup >= sup (rng (G . j)) by YELLOW_2:def_5;
hence Sup >= Sup by YELLOW_2:def_5; ::_thesis: verum
end;
A5: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) holds
Inf >= Inf
proof
let f be V9() ManySortedSet of J; ::_thesis: ( f in Funcs (J,(Fin K)) implies 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
Inf >= Inf )
assume A6: f in Funcs (J,(Fin K)) ; ::_thesis: 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
Inf >= Inf
let G be DoubleIndexedSet of f,L; ::_thesis: ( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) ) implies Inf >= Inf )
assume A7: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) ; ::_thesis: Inf >= Inf
rng (Sups ) is_>=_than Inf
proof
let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in rng (Sups ) or Inf <= a )
assume a in rng (Sups ) ; ::_thesis: Inf <= a
then consider j being Element of J such that
A8: a = Sup by Th14;
Sup in rng (Sups ) by Th14;
then Sup >= inf (rng (Sups )) by YELLOW_2:22;
then A9: Sup >= Inf by YELLOW_2:def_6;
Sup >= Sup by A1, A6, A7;
hence Inf <= a by A8, A9, ORDERS_2:3; ::_thesis: verum
end;
then inf (rng (Sups )) >= Inf by YELLOW_0:33;
hence Inf >= Inf by YELLOW_2:def_6; ::_thesis: verum
end;
assume A10: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } ; ::_thesis: Inf >= sup X
Inf is_>=_than X
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <= Inf )
assume a in X ; ::_thesis: a <= Inf
then ex a9 being Element of L st
( a9 = a & 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a9 = Inf ) ) ) by A10;
hence a <= Inf by A5; ::_thesis: verum
end;
hence Inf >= sup X by YELLOW_0:32; ::_thesis: verum
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 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X
proof
let L be complete LATTICE; ::_thesis: ( L is continuous implies 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X )
assume A1: L is continuous ; ::_thesis: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X
hereby ::_thesis: verum
let J, K be non empty set ; ::_thesis: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X
set FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } ;
set k = the Element of K;
{ the Element of K} in { A where A is Subset of K : ( A is finite & A <> {} ) } ;
then reconsider FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } as non empty set ;
let F be Function of [:J,K:], the carrier of L; ::_thesis: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X
let X be Subset of L; ::_thesis: ( 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } implies Inf = sup X )
set N = Funcs (J,FIK);
deffunc H1( Element of J, Element of Funcs (J,FIK)) -> Element of the carrier of L = sup (((curry F) . $1) .: ($2 . $1));
ex H being Function of [:J,(Funcs (J,FIK)):], the carrier of L st
for j being Element of J
for g being Element of Funcs (J,FIK) holds H . (j,g) = H1(j,g) from BINOP_1:sch_4();
then consider H being Function of [:J,(Funcs (J,FIK)):], the carrier of L such that
A2: for j being Element of J
for g being Element of Funcs (J,FIK) holds H . (j,g) = sup (((curry F) . j) .: (g . j)) ;
set cF = curry F;
set cH = curry H;
A3: for j being Element of J holds
( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j) ) )
proof
let j be Element of J; ::_thesis: ( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j) ) )
set D = rng ((curry H) . j);
set R = rng ((curry F) . j);
set Hj = (curry H) . j;
set Fj = (curry F) . j;
thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L by YELLOW_0:17; ::_thesis: ( ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j) ) )
thus for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ::_thesis: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j)
proof
let x be Element of L; ::_thesis: ( x in rng ((curry H) . j) implies ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) )
assume x in rng ((curry H) . j) ; ::_thesis: ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) )
then consider g being set such that
A4: g in dom ((curry H) . j) and
A5: ((curry H) . j) . g = x by FUNCT_1:def_3;
reconsider g = g as Element of Funcs (J,FIK) by A4, Th20;
g . j in FIK ;
then ex A being Subset of K st
( A = g . j & A is finite & A <> {} ) ;
then reconsider Y = ((curry F) . j) .: (g . j) as finite Subset of (rng ((curry F) . j)) by RELAT_1:111;
take Y ; ::_thesis: ( ex_sup_of Y,L & x = "\/" (Y,L) )
x = H . (j,g) by A5, Th20
.= sup (((curry F) . j) .: (g . j)) by A2 ;
hence ( ex_sup_of Y,L & x = "\/" (Y,L) ) by YELLOW_0:17; ::_thesis: verum
end;
thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j) ::_thesis: verum
proof
let Y be finite Subset of (rng ((curry F) . j)); ::_thesis: ( Y <> {} implies "\/" (Y,L) in rng ((curry H) . j) )
consider Z being set such that
A6: Z c= dom ((curry F) . j) and
A7: Z is finite and
A8: ((curry F) . j) .: Z = Y by ORDERS_1:85;
A9: Z c= K by A6, Th20;
assume Y <> {} ; ::_thesis: "\/" (Y,L) in rng ((curry H) . j)
then Z <> {} by A8;
then Z in FIK by A7, A9;
then A10: {Z} c= FIK by ZFMISC_1:31;
( dom (J --> Z) = J & rng (J --> Z) = {Z} ) by FUNCOP_1:8, FUNCOP_1:13;
then reconsider g = J --> Z as Element of Funcs (J,FIK) by A10, FUNCT_2:def_2;
A11: g . j = Z by FUNCOP_1:7;
g in Funcs (J,FIK) ;
then A12: g in dom ((curry H) . j) by Th20;
((curry H) . j) . g = H . (j,g) by Th20
.= "\/" (Y,L) by A2, A8, A11 ;
hence "\/" (Y,L) in rng ((curry H) . j) by A12, FUNCT_1:def_3; ::_thesis: verum
end;
end;
for j being Element of J holds rng ((curry H) . j) is directed
proof
let j be Element of J; ::_thesis: rng ((curry H) . j) is directed
A13: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j) by A3;
( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) ) by A3;
hence rng ((curry H) . j) is directed by A13, WAYBEL_0:51; ::_thesis: verum
end;
then A14: Inf = Sup by A1, Lm8;
A15: for j being set st j in dom (curry F) holds
\\/ (((curry F) . j),L) = \\/ (((curry H) . j),L)
proof
let j9 be set ; ::_thesis: ( j9 in dom (curry F) implies \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) )
assume j9 in dom (curry F) ; ::_thesis: \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L)
then reconsider j = j9 as Element of J ;
A16: ( ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" (Y,L) in rng ((curry H) . j) ) ) by A3;
( ex_sup_of rng ((curry F) . j),L & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) ) by YELLOW_0:17;
then sup (rng ((curry F) . j)) = sup (rng ((curry H) . j)) by A16, WAYBEL_0:54;
then Sup = sup (rng ((curry H) . j)) by YELLOW_2:def_5;
hence \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) by YELLOW_2:def_5; ::_thesis: verum
end;
assume A17: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } ; ::_thesis: Inf = sup X
then A18: Inf >= sup X by Th22;
A19: FIK c= Fin K
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FIK or x in Fin K )
assume x in FIK ; ::_thesis: x in Fin K
then ex A being Subset of K st
( x = A & A is finite & A <> {} ) ;
hence x in Fin K by FINSUB_1:def_5; ::_thesis: verum
end;
A20: for h being Function-yielding Function st h in product (doms (curry H)) holds
( ( for j being Element of J holds
( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )
proof
let h be Function-yielding Function; ::_thesis: ( h in product (doms (curry H)) implies ( ( for j being Element of J holds
( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) )
set f = (Frege h) . (id J);
assume h in product (doms (curry H)) ; ::_thesis: ( ( for j being Element of J holds
( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )
then A21: h in dom (Frege (curry H)) by PARTFUN1:def_2;
then A22: dom h = dom (curry H) by Th8
.= J by Th20 ;
A23: for x being set st x in dom (doms h) holds
(id J) . x in (doms h) . x
proof
let x be set ; ::_thesis: ( x in dom (doms h) implies (id J) . x in (doms h) . x )
assume x in dom (doms h) ; ::_thesis: (id J) . x in (doms h) . x
then reconsider j = x as Element of J by A22, FUNCT_6:59;
h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;
then h . j in Funcs (J,FIK) by FUNCOP_1:7;
then ex g being Function st
( g = h . j & dom g = J & rng g c= FIK ) by FUNCT_2:def_2;
then ( (id J) . j = j & (doms h) . j = J ) by A22, FUNCT_1:18, FUNCT_6:22;
hence (id J) . x in (doms h) . x ; ::_thesis: verum
end;
( dom (id J) = J & dom (doms h) = dom h ) by FUNCT_6:59;
then id J in product (doms h) by A22, A23, CARD_3:9;
then A24: id J in dom (Frege h) by PARTFUN1:def_2;
then A25: dom ((Frege h) . (id J)) = J by A22, Th8;
then reconsider f9 = (Frege h) . (id J) as ManySortedSet of J by PARTFUN1:def_2, RELAT_1:def_18;
thus A26: for j being Element of J holds
( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ::_thesis: ( (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )
proof
let j be Element of J; ::_thesis: ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K )
thus A27: ((Frege h) . (id J)) . j = (h . j) . ((id J) . j) by A22, A24, Th9
.= (h . j) . j by FUNCT_1:18 ; ::_thesis: ( h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K )
h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;
hence h . j in Funcs (J,FIK) by FUNCOP_1:7; ::_thesis: ((Frege h) . (id J)) . j is non empty finite Subset of K
then consider g being Function such that
A28: ( g = h . j & dom g = J ) and
A29: rng g c= FIK by FUNCT_2:def_2;
((Frege h) . (id J)) . j in rng g by A27, A28, FUNCT_1:def_3;
then ((Frege h) . (id J)) . j in FIK by A29;
then ex A being Subset of K st
( ((Frege h) . (id J)) . j = A & A is finite & A <> {} ) ;
hence ((Frege h) . (id J)) . j is non empty finite Subset of K ; ::_thesis: verum
end;
then for j being set st j in J holds
not f9 . j is empty ;
hence (Frege h) . (id J) is V9() ManySortedSet of J by PBOOLE:def_13; ::_thesis: ( (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )
A30: rng ((Frege h) . (id J)) c= FIK
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((Frege h) . (id J)) or y in FIK )
assume y in rng ((Frege h) . (id J)) ; ::_thesis: y in FIK
then consider j being set such that
A31: j in dom ((Frege h) . (id J)) and
A32: y = ((Frege h) . (id J)) . j by FUNCT_1:def_3;
((Frege h) . (id J)) . j is non empty finite Subset of K by A26, A25, A31;
hence y in FIK by A32; ::_thesis: verum
end;
hence (Frege h) . (id J) in Funcs (J,FIK) by A25, FUNCT_2:def_2; ::_thesis: (Frege h) . (id J) in Funcs (J,(Fin K))
rng ((Frege h) . (id J)) c= Fin K by A19, A30, XBOOLE_1:1;
hence (Frege h) . (id J) in Funcs (J,(Fin K)) by A25, FUNCT_2:def_2; ::_thesis: verum
end;
A33: for h being Element of product (doms (curry H)) holds Inf <= sup X
proof
defpred S1[ set , set , set ] means $1 = F . ($3,$2);
let h be Element of product (doms (curry H)); ::_thesis: Inf <= sup X
h in product (doms (curry H)) ;
then A34: h in dom (Frege (curry H)) by PARTFUN1:def_2;
for x being set st x in dom h holds
h . x is Function
proof
let x be set ; ::_thesis: ( x in dom h implies h . x is Function )
assume A35: x in dom h ; ::_thesis: h . x is Function
dom h = dom (curry H) by A34, Th8
.= J by Th20 ;
then reconsider j = x as Element of J by A35;
h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6;
then h . j in Funcs (J,FIK) by FUNCOP_1:7;
hence h . x is Function ; ::_thesis: verum
end;
then reconsider h9 = h as Function-yielding Function by FUNCOP_1:def_6;
reconsider f = (Frege h9) . (id J) as V9() ManySortedSet of J by A20;
A36: for j being set st j in J holds
for x being set st x in f . j holds
ex y being set st
( y in (J --> the carrier of L) . j & S1[y,x,j] )
proof
let i be set ; ::_thesis: ( i in J implies for x being set st x in f . i holds
ex y being set st
( y in (J --> the carrier of L) . i & S1[y,x,i] ) )
assume i in J ; ::_thesis: for x being set st x in f . i holds
ex y being set st
( y in (J --> the carrier of L) . i & S1[y,x,i] )
then reconsider j = i as Element of J ;
let x be set ; ::_thesis: ( x in f . i implies ex y being set st
( y in (J --> the carrier of L) . i & S1[y,x,i] ) )
assume A37: x in f . i ; ::_thesis: ex y being set st
( y in (J --> the carrier of L) . i & S1[y,x,i] )
f . j is Subset of K by A20;
then reconsider k = x as Element of K by A37;
take y = F . [j,k]; ::_thesis: ( y in (J --> the carrier of L) . i & S1[y,x,i] )
y in the carrier of L ;
hence ( y in (J --> the carrier of L) . i & S1[y,x,i] ) by FUNCOP_1:7; ::_thesis: verum
end;
ex G being ManySortedFunction of f,J --> the carrier of L st
for j being set st j in J holds
ex g being Function of (f . j),((J --> the carrier of L) . j) st
( g = G . j & ( for x being set st x in f . j holds
S1[g . x,x,j] ) ) from MSSUBFAM:sch_1(A36);
then consider G being ManySortedFunction of f,J --> the carrier of L such that
A38: for j being set st j in J holds
ex g being Function of (f . j),((J --> the carrier of L) . j) st
( g = G . j & ( for x being set st x in f . j holds
g . x = F . (j,x) ) ) ;
reconsider G = G as DoubleIndexedSet of f,L ;
A39: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x)
proof
let j be Element of J; ::_thesis: for x being set st x in f . j holds
(G . j) . x = F . (j,x)
let x be set ; ::_thesis: ( x in f . j implies (G . j) . x = F . (j,x) )
assume A40: x in f . j ; ::_thesis: (G . j) . x = F . (j,x)
ex g being Function of (f . j),((J --> the carrier of L) . j) st
( g = G . j & ( for x being set st x in f . j holds
g . x = F . (j,x) ) ) by A38;
hence (G . j) . x = F . (j,x) by A40; ::_thesis: verum
end;
Inf is_<=_than rng (Sups )
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in rng (Sups ) or Inf <= y )
assume y in rng (Sups ) ; ::_thesis: Inf <= y
then consider j being Element of J such that
A41: y = Sup by Th14;
j in J ;
then A42: j in dom (curry H) by Th20;
A43: ((curry F) . j) .: (f . j) c= rng (G . j)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((curry F) . j) .: (f . j) or y in rng (G . j) )
assume y in ((curry F) . j) .: (f . j) ; ::_thesis: y in rng (G . j)
then consider x being set such that
A44: x in dom ((curry F) . j) and
A45: x in f . j and
A46: y = ((curry F) . j) . x by FUNCT_1:def_6;
reconsider k = x as Element of K by A44, Th20;
A47: k in dom (G . j) by A45, FUNCT_2:def_1;
y = F . (j,k) by A46, Th20
.= (G . j) . k by A39, A45 ;
hence y in rng (G . j) by A47, FUNCT_1:def_3; ::_thesis: verum
end;
( ex_sup_of ((curry F) . j) .: (f . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;
then sup (((curry F) . j) .: (f . j)) <= sup (rng (G . j)) by A43, YELLOW_0:34;
then A48: sup (((curry F) . j) .: (f . j)) <= Sup by YELLOW_2:def_5;
h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6;
then reconsider hj = h . j as Element of Funcs (J,FIK) by FUNCOP_1:7;
A49: Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:53;
sup (((curry F) . j) .: (f . j)) = sup (((curry F) . j) .: (hj . j)) by A20
.= H . (j,hj) by A2
.= ((curry H) . j) . (h . j) by Th20
.= ((Frege (curry H)) . h) . j by A34, A42, Th9 ;
hence Inf <= y by A41, A48, A49, ORDERS_2:3; ::_thesis: verum
end;
then Inf <= inf (rng (Sups )) by YELLOW_0:33;
then A50: Inf <= Inf by YELLOW_2:def_6;
f in Funcs (J,(Fin K)) by A20;
then Inf in X by A17, A39;
then Inf <= sup X by YELLOW_2:22;
hence Inf <= sup X by A50, ORDERS_2:3; ::_thesis: verum
end;
rng (Infs ) is_<=_than sup X
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in rng (Infs ) or x <= sup X )
assume x in rng (Infs ) ; ::_thesis: x <= sup X
then consider h being set such that
A51: h in dom (Frege (curry H)) and
A52: x = //\ (((Frege (curry H)) . h),L) by Th13;
reconsider h = h as Element of product (doms (curry H)) by A51;
Inf <= sup X by A33;
hence x <= sup X by A52; ::_thesis: verum
end;
then A53: sup (rng (Infs )) <= sup X by YELLOW_0:32;
dom (curry F) = J by Th20
.= dom (curry H) by Th20 ;
then Inf = Inf by A15, Th11;
then Inf <= sup X by A14, A53, YELLOW_2:def_5;
hence Inf = sup X by A18, ORDERS_2:2; ::_thesis: verum
end;
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 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X ) holds
L is continuous
proof
let L be complete LATTICE; ::_thesis: ( ( 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X ) implies L is continuous )
assume A1: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X ; ::_thesis: L is continuous
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
proof
let J, K be non empty set ; ::_thesis: 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
let F be Function of [:J,K:], the carrier of L; ::_thesis: ( ( for j being Element of J holds rng ((curry F) . j) is directed ) implies Inf = Sup )
assume A2: for j being Element of J holds rng ((curry F) . j) is directed ; ::_thesis: Inf = Sup
defpred S1[ Element of L] means 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & $1 = Inf ) );
reconsider X = { a where a is Element of L : S1[a] } as Subset of L from DOMAIN_1:sch_7();
X is_<=_than Sup
proof
let a9 be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a9 in X or a9 <= Sup )
assume a9 in X ; ::_thesis: a9 <= Sup
then consider a being Element of L such that
A3: a9 = a and
A4: 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) ;
defpred S2[ set , set ] means ( $1 in J & $2 in K & ex b being Element of L st
( b = ((curry F) . $1) . $2 & a <= b ) );
consider f being V9() ManySortedSet of J such that
A5: f in Funcs (J,(Fin K)) and
A6: 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 ) by A4;
consider G being DoubleIndexedSet of f,L such that
A7: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . (j,x) and
A8: a = Inf by A6;
A9: for x being set st x in J holds
ex y being set st
( y in K & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in J implies ex y being set st
( y in K & S2[x,y] ) )
assume x in J ; ::_thesis: ex y being set st
( y in K & S2[x,y] )
then reconsider j = x as Element of J ;
Sup in rng (Sups ) by Th14;
then inf (rng (Sups )) <= Sup by YELLOW_2:22;
then A10: Inf <= Sup by YELLOW_2:def_6;
( not rng ((curry F) . j) is empty & rng ((curry F) . j) is directed & rng (G . j) is finite Subset of (rng ((curry F) . j)) ) by A2, A5, A7, Lm12;
then consider y being Element of L such that
A11: y in rng ((curry F) . j) and
A12: rng (G . j) is_<=_than y by WAYBEL_0:1;
consider k being set such that
A13: k in dom ((curry F) . j) and
A14: y = ((curry F) . j) . k by A11, FUNCT_1:def_3;
reconsider k = k as Element of K by A13, Th20;
take k ; ::_thesis: ( k in K & S2[x,k] )
sup (rng (G . j)) <= y by A12, YELLOW_0:32;
then Sup <= y by YELLOW_2:def_5;
hence ( k in K & S2[x,k] ) by A8, A14, A10, ORDERS_2:3; ::_thesis: verum
end;
consider g being Function such that
A15: dom g = J and
rng g c= K and
A16: for x being set st x in J holds
S2[x,g . x] from FUNCT_1:sch_5(A9);
A17: dom (doms (curry F)) = dom (curry F) by FUNCT_6:59;
then A18: dom g = dom (doms (curry F)) by A15, Th20;
for x being set st x in dom (doms (curry F)) holds
g . x in (doms (curry F)) . x
proof
let x be set ; ::_thesis: ( x in dom (doms (curry F)) implies g . x in (doms (curry F)) . x )
assume x in dom (doms (curry F)) ; ::_thesis: g . x in (doms (curry F)) . x
then reconsider j = x as Element of J by A17;
dom (curry F) = J by Th20;
then (doms (curry F)) . j = dom ((curry F) . j) by FUNCT_6:22
.= K by Th20 ;
hence g . x in (doms (curry F)) . x by A16; ::_thesis: verum
end;
then reconsider g = g as Element of product (doms (curry F)) by A18, CARD_3:9;
for j being Element of J holds a <= ((Frege (curry F)) . g) . j
proof
let j be Element of J; ::_thesis: a <= ((Frege (curry F)) . g) . j
A19: ex b being Element of L st
( b = ((curry F) . j) . (g . j) & a <= b ) by A16;
( dom (Frege (curry F)) = product (doms (curry F)) & J = dom (curry F) ) by PARTFUN1:def_2;
hence a <= ((Frege (curry F)) . g) . j by A19, Th9; ::_thesis: verum
end;
then A20: a <= Inf by YELLOW_2:55;
Inf in rng (Infs ) by Th14;
then Inf <= sup (rng (Infs )) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def_5;
hence a9 <= Sup by A3, A20, ORDERS_2:3; ::_thesis: verum
end;
then sup X <= Sup by YELLOW_0:32;
then A21: Inf <= Sup by A1;
Inf >= Sup by Th16;
hence Inf = Sup by A21, ORDERS_2:2; ::_thesis: verum
end;
hence L is continuous by Lm10; ::_thesis: verum
end;
theorem :: WAYBEL_5:23
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 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X ) by Lm13, Lm14;
begin
definition
let L be non empty RelStr ;
attrL is completely-distributive means :Def3: :: WAYBEL_5:def 3
( L is complete & ( for J being non empty set
for K being V9() 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 V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) );
registration
cluster1 -element reflexive transitive antisymmetric -> 1 -element completely-distributive for RelStr ;
coherence
for b1 being 1 -element Poset holds b1 is completely-distributive
proof
let L be 1 -element Poset; ::_thesis: L is completely-distributive
reconsider L9 = L as complete LATTICE ;
thus L is complete ; :: according to WAYBEL_5:def_3 ::_thesis: for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup
reconsider L9 = L9 as continuous LATTICE ;
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L9 holds Inf = Sup
proof
let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L9 holds Inf = Sup
let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L9 holds Inf = Sup
let F be DoubleIndexedSet of K,L9; ::_thesis: Inf = Sup
for j being Element of J holds rng (F . j) is directed ;
hence Inf = Sup by Lm8; ::_thesis: verum
end;
hence for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ; ::_thesis: verum
end;
end;
registration
cluster non empty total reflexive transitive antisymmetric with_suprema with_infima completely-distributive for RelStr ;
existence
ex b1 being LATTICE st b1 is completely-distributive
proof
set x = the set ;
set R = the Order of { the set };
RelStr(# { the set }, the Order of { the set } #) is 1 -element RelStr ;
hence ex b1 being LATTICE st b1 is completely-distributive ; ::_thesis: verum
end;
end;
theorem Th24: :: WAYBEL_5:24
for L being completely-distributive LATTICE holds L is continuous
proof
let L be completely-distributive LATTICE; ::_thesis: L is continuous
A1: 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 by Def3;
L is complete by Def3;
hence L is continuous by A1, Lm9; ::_thesis: verum
end;
registration
cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> complete continuous for 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 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
let L be non empty transitive antisymmetric with_infima RelStr ; ::_thesis: 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
let x be Element of L; ::_thesis: 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
let X, Y be Subset of L; ::_thesis: ( ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } implies x "/\" (sup X) >= sup Y )
assume that
A1: ex_sup_of X,L and
A2: ex_sup_of Y,L and
A3: Y = { (x "/\" y) where y is Element of L : y in X } ; ::_thesis: x "/\" (sup X) >= sup Y
Y is_<=_than x "/\" (sup X)
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in Y or y <= x "/\" (sup X) )
assume y in Y ; ::_thesis: y <= x "/\" (sup X)
then consider z being Element of L such that
A4: y = x "/\" z and
A5: z in X by A3;
A6: y <= z by A4, YELLOW_0:23;
X is_<=_than sup X by A1, YELLOW_0:30;
then z <= sup X by A5, LATTICE3:def_9;
then A7: y <= sup X by A6, YELLOW_0:def_2;
y <= x by A4, YELLOW_0:23;
hence y <= x "/\" (sup X) by A7, YELLOW_0:23; ::_thesis: verum
end;
hence x "/\" (sup X) >= sup Y by A2, YELLOW_0:30; ::_thesis: verum
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
let L be completely-distributive LATTICE; ::_thesis: 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)
let X be non empty Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
let x be Element of L; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
set A = { (x "/\" y) where y is Element of L : y in X } ;
set J = {1,2};
set K = (1,2) --> ({1},X);
set F = (1,2) --> (({1} --> x),(id X));
A1: ((1,2) --> (({1} --> x),(id X))) . 1 = {1} --> x by FUNCT_4:63;
A2: dom ((1,2) --> ({1},X)) = {1,2} by FUNCT_4:62;
A3: ((1,2) --> ({1},X)) . 2 = X by FUNCT_4:63;
A4: dom ((1,2) --> (({1} --> x),(id X))) = {1,2} by FUNCT_4:62;
reconsider j1 = 1, j2 = 2 as Element of {1,2} by TARSKI:def_2;
A5: ((1,2) --> (({1} --> x),(id X))) . 2 = id X by FUNCT_4:63;
reconsider F = (1,2) --> (({1} --> x),(id X)) as ManySortedSet of {1,2} by A4, PARTFUN1:def_2, RELAT_1:def_18;
A6: ((1,2) --> ({1},X)) . 1 = {1} by FUNCT_4:63;
reconsider K = (1,2) --> ({1},X) as ManySortedSet of {1,2} by A2, PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in {1,2} holds
not K . i is empty by A6, A3, TARSKI:def_2;
then reconsider K = K as V9() ManySortedSet of {1,2} by PBOOLE:def_13;
for j being set st j in {1,2} holds
F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
proof
let j be set ; ::_thesis: ( j in {1,2} implies F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) )
assume A7: j in {1,2} ; ::_thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
then A8: ({1,2} --> the carrier of L) . j = the carrier of L by FUNCOP_1:7;
percases ( j = 1 or j = 2 ) by A7, TARSKI:def_2;
suppose j = 1 ; ::_thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
hence F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) by A1, A6, A7, FUNCOP_1:7; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
hence F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) by A5, A3, A8, FUNCT_2:7; ::_thesis: verum
end;
end;
end;
then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def_15;
rng (Infs ) is_<=_than "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in rng (Infs ) or y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) )
assume y in rng (Infs ) ; ::_thesis: y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
then consider f being set such that
A9: f in dom (Frege F) and
A10: y = //\ (((Frege F) . f),L) by Th13;
reconsider f = f as Function by A9;
A11: f . j2 in K . j2 by A9, Lm6;
then reconsider f2 = f . 2 as Element of X by FUNCT_4:63;
A12: f . j1 in K . j1 by A9, Lm6;
A13: {x,f2} c= rng ((Frege F) . f)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,f2} or z in rng ((Frege F) . f) )
assume z in {x,f2} ; ::_thesis: z in rng ((Frege F) . f)
then ( z = x or z = f . 2 ) by TARSKI:def_2;
then ( z = (F . j1) . (f . j1) or z = (F . j2) . (f . j2) ) by A1, A5, A6, A3, A12, A11, FUNCOP_1:7, FUNCT_1:18;
hence z in rng ((Frege F) . f) by A9, Lm5; ::_thesis: verum
end;
x "/\" f2 in { (x "/\" y) where y is Element of L : y in X } ;
then A14: x "/\" f2 <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_2:22;
A15: ( ex_inf_of rng ((Frege F) . f),L & ex_inf_of {x,(f . 2)},L ) by YELLOW_0:17;
y = "/\" ((rng ((Frege F) . f)),L) by A10, YELLOW_2:def_6;
then y <= inf {x,f2} by A15, A13, YELLOW_0:35;
then y <= x "/\" f2 by YELLOW_0:40;
hence y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A14, YELLOW_0:def_2; ::_thesis: verum
end;
then sup (rng (Infs )) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_0:32;
then A16: Sup <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_2:def_5;
(x "/\") .: X = { (x "/\" y) where y is Element of L : y in X } by WAYBEL_1:61;
then reconsider A9 = { (x "/\" y) where y is Element of L : y in X } as Subset of L ;
( ex_sup_of X,L & ex_sup_of A9,L ) by YELLOW_0:17;
then A17: x "/\" (sup X) >= sup A9 by Th25;
x "/\" (sup X) is_<=_than rng (Sups )
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in rng (Sups ) or x "/\" (sup X) <= y )
assume y in rng (Sups ) ; ::_thesis: x "/\" (sup X) <= y
then consider j being Element of {1,2} such that
A18: y = Sup by Th14;
percases ( j = 1 or j = 2 ) by TARSKI:def_2;
suppose j = 1 ; ::_thesis: x "/\" (sup X) <= y
then rng (F . j) = {x} by A1, FUNCOP_1:8;
then Sup = sup {x} by YELLOW_2:def_5;
then y = x by A18, YELLOW_0:39;
hence x "/\" (sup X) <= y by YELLOW_0:23; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: x "/\" (sup X) <= y
then rng (F . j) = X by A5, RELAT_1:45;
then y = sup X by A18, YELLOW_2:def_5;
hence x "/\" (sup X) <= y by YELLOW_0:23; ::_thesis: verum
end;
end;
end;
then x "/\" (sup X) <= inf (rng (Sups )) by YELLOW_0:33;
then x "/\" (sup X) <= Inf by YELLOW_2:def_6;
then x "/\" (sup X) <= Sup by Def3;
then x "/\" (sup X) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A16, YELLOW_0:def_2;
hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A17, YELLOW_0:def_3; ::_thesis: verum
end;
theorem Th26: :: WAYBEL_5:26
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
let L be completely-distributive LATTICE; ::_thesis: 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)
let X be Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
let x be Element of L; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
set A = { (x "/\" y) where y is Element of L : y in X } ;
percases ( X is empty or not X is empty ) ;
supposeA1: X is empty ; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
now__::_thesis:_not__{__(x_"/\"_y)_where_y_is_Element_of_L_:_y_in_X__}__<>_{}
set z = the Element of { (x "/\" y) where y is Element of L : y in X } ;
assume { (x "/\" y) where y is Element of L : y in X } <> {} ; ::_thesis: contradiction
then the Element of { (x "/\" y) where y is Element of L : y in X } in { (x "/\" y) where y is Element of L : y in X } ;
then ex y being Element of L st
( the Element of { (x "/\" y) where y is Element of L : y in X } = x "/\" y & y in X ) ;
hence contradiction by A1; ::_thesis: verum
end;
then A2: "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) = Bottom L by YELLOW_0:def_11;
sup X = Bottom L by A1, YELLOW_0:def_11;
hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A2, WAYBEL_1:3; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by Lm15; ::_thesis: verum
end;
end;
end;
registration
cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> Heyting for RelStr ;
correctness
coherence
for b1 being LATTICE st b1 is completely-distributive holds
b1 is Heyting ;
proof
let L be LATTICE; ::_thesis: ( L is completely-distributive implies L is Heyting )
assume L is completely-distributive ; ::_thesis: L is Heyting
then reconsider L = L as 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) by Th26;
then for x being Element of L holds x "/\" is lower_adjoint by WAYBEL_1:64;
hence L is Heyting by WAYBEL_1:def_19; ::_thesis: verum
end;
end;
begin
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
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 st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
proof
let L be complete LATTICE; ::_thesis: 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
rng (Infs ) is directed
let J be non empty set ; ::_thesis: 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
rng (Infs ) is directed
let K be V9() ManySortedSet of J; ::_thesis: 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
let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies rng (Infs ) is directed )
set X = rng (Infs );
assume A1: for j being Element of J holds rng (F . j) is directed ; ::_thesis: rng (Infs ) is directed
for x, y being Element of L st x in rng (Infs ) & y in rng (Infs ) holds
ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )
proof
let x, y be Element of L; ::_thesis: ( x in rng (Infs ) & y in rng (Infs ) implies ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z ) )
assume that
A2: x in rng (Infs ) and
A3: y in rng (Infs ) ; ::_thesis: ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )
consider h being set such that
A4: h in dom (Frege F) and
A5: y = //\ (((Frege F) . h),L) by A3, Th13;
reconsider h = h as Function by A4;
reconsider H = (Frege F) . h as Function of J, the carrier of L by A4, Th10;
consider g being set such that
A6: g in dom (Frege F) and
A7: x = //\ (((Frege F) . g),L) by A2, Th13;
reconsider g = g as Function by A6;
reconsider G = (Frege F) . g as Function of J, the carrier of L by A6, Th10;
A8: ex_inf_of rng ((Frege F) . g),L by YELLOW_0:17;
defpred S1[ set , set ] means ( $1 in J & $2 in K . $1 & ( for c being Element of L st c = (F . $1) . $2 holds
( ( for a being Element of L st a = G . $1 holds
a <= c ) & ( for b being Element of L st b = H . $1 holds
b <= c ) ) ) );
A9: for j being Element of J ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )
proof
let j be Element of J; ::_thesis: ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )
j in J ;
then A10: j in dom F by PARTFUN1:def_2;
then A11: g . j in dom (F . j) by A6, Th9;
j in J ;
then A12: j in dom F by PARTFUN1:def_2;
then G . j = (F . j) . (g . j) by A6, Th9;
then A13: G . j in rng (F . j) by A11, FUNCT_1:def_3;
A14: h . j in dom (F . j) by A4, A10, Th9;
H . j = (F . j) . (h . j) by A4, A12, Th9;
then A15: H . j in rng (F . j) by A14, FUNCT_1:def_3;
rng (F . j) is directed Subset of L by A1;
then consider c being Element of L such that
A16: c in rng (F . j) and
A17: ( G . j <= c & H . j <= c ) by A13, A15, WAYBEL_0:def_1;
consider k being set such that
A18: k in dom (F . j) and
A19: c = (F . j) . k by A16, FUNCT_1:def_3;
reconsider k = k as Element of K . j by A18;
take k ; ::_thesis: ( G . j <= (F . j) . k & H . j <= (F . j) . k )
thus ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A17, A19; ::_thesis: verum
end;
A20: for j being set st j in J holds
ex k being set st
( k in union (rng K) & S1[j,k] )
proof
let j9 be set ; ::_thesis: ( j9 in J implies ex k being set st
( k in union (rng K) & S1[j9,k] ) )
assume j9 in J ; ::_thesis: ex k being set st
( k in union (rng K) & S1[j9,k] )
then reconsider j = j9 as Element of J ;
consider k being Element of K . j such that
A21: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A9;
take k ; ::_thesis: ( k in union (rng K) & S1[j9,k] )
j in J ;
then j in dom K by PARTFUN1:def_2;
then K . j in rng K by FUNCT_1:def_3;
hence k in union (rng K) by TARSKI:def_4; ::_thesis: S1[j9,k]
thus S1[j9,k] by A21; ::_thesis: verum
end;
consider f being Function such that
A22: dom f = J and
rng f c= union (rng K) and
A23: for j being set st j in J holds
S1[j,f . j] from FUNCT_1:sch_5(A20);
A24: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_F)_holds_
f_._x_in_(doms_F)_._x
let x be set ; ::_thesis: ( x in dom (doms F) implies f . x in (doms F) . x )
assume x in dom (doms F) ; ::_thesis: f . x in (doms F) . x
then A25: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J ;
(doms F) . x = dom (F . j) by A25, FUNCT_6:22
.= K . j by FUNCT_2:def_1 ;
hence f . x in (doms F) . x by A23; ::_thesis: verum
end;
dom f = dom F by A22, PARTFUN1:def_2
.= dom (doms F) by FUNCT_6:59 ;
then f in product (doms F) by A24, CARD_3:9;
then A26: f in dom (Frege F) by PARTFUN1:def_2;
then reconsider Ff = (Frege F) . f as Function of J, the carrier of L by Th10;
take z = Inf ; ::_thesis: ( z in rng (Infs ) & x <= z & y <= z )
thus z in rng (Infs ) by A26, Th13; ::_thesis: ( x <= z & y <= z )
A27: x = "/\" ((rng ((Frege F) . g)),L) by A7, YELLOW_2:def_6;
now__::_thesis:_for_j_being_Element_of_J_holds_x_<=_Ff_._j
let j be Element of J; ::_thesis: x <= Ff . j
A28: j in J ;
then j in dom G by FUNCT_2:def_1;
then A29: G . j in rng G by FUNCT_1:def_3;
j in dom F by A28, PARTFUN1:def_2;
then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;
then A30: G . j <= Ff . j by A23;
x is_<=_than rng G by A27, A8, YELLOW_0:def_10;
then x <= G . j by A29, LATTICE3:def_8;
hence x <= Ff . j by A30, ORDERS_2:3; ::_thesis: verum
end;
hence x <= z by YELLOW_2:55; ::_thesis: y <= z
A31: ex_inf_of rng ((Frege F) . h),L by YELLOW_0:17;
A32: y = "/\" ((rng ((Frege F) . h)),L) by A5, YELLOW_2:def_6;
now__::_thesis:_for_j_being_Element_of_J_holds_y_<=_Ff_._j
let j be Element of J; ::_thesis: y <= Ff . j
A33: j in J ;
then j in dom H by FUNCT_2:def_1;
then A34: H . j in rng H by FUNCT_1:def_3;
j in dom F by A33, PARTFUN1:def_2;
then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;
then A35: H . j <= Ff . j by A23;
y is_<=_than rng H by A32, A31, YELLOW_0:def_10;
then y <= H . j by A34, LATTICE3:def_8;
hence y <= Ff . j by A35, ORDERS_2:3; ::_thesis: verum
end;
hence y <= z by YELLOW_2:55; ::_thesis: verum
end;
hence rng (Infs ) is directed by WAYBEL_0:def_1; ::_thesis: verum
end;
theorem :: WAYBEL_5:28
for L being complete LATTICE st L is continuous holds
for S being CLSubFrame of L holds S is continuous LATTICE
proof
let L be complete LATTICE; ::_thesis: ( L is continuous implies for S being CLSubFrame of L holds S is continuous LATTICE )
assume A1: L is continuous ; ::_thesis: for S being CLSubFrame of L holds S is continuous LATTICE
let S be CLSubFrame of L; ::_thesis: S is continuous LATTICE
reconsider L9 = L as complete LATTICE ;
A2: S is complete LATTICE by YELLOW_2:30;
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
proof
let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,S; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A3: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup
now__::_thesis:_for_j_being_set_st_j_in_J_holds_
F_._j_is_Function_of_(K_._j),((J_-->_the_carrier_of_L)_._j)
let j be set ; ::_thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) )
assume A4: j in J ; ::_thesis: F . j is Function of (K . j),((J --> the carrier of L) . j)
then reconsider j9 = j as Element of J ;
A5: ( F . j9 is Function of (K . j9), the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def_13;
(J --> the carrier of L) . j = the carrier of L by A4, FUNCOP_1:7;
hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A5, FUNCT_2:7; ::_thesis: verum
end;
then reconsider F9 = F as DoubleIndexedSet of K,L by PBOOLE:def_15;
ex_inf_of rng (Sups ),L by YELLOW_0:17;
then A6: "/\" ((rng (Sups )),L) in the carrier of S by YELLOW_0:def_18;
now__::_thesis:_for_x_being_set_st_x_in_rng_(Sups_)_holds_
x_in_rng_(Sups_)
let x be set ; ::_thesis: ( x in rng (Sups ) implies x in rng (Sups ) )
assume x in rng (Sups ) ; ::_thesis: x in rng (Sups )
then consider j being Element of J such that
A7: x = Sup by Th14;
A8: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17;
x = sup (rng (F9 . j)) by A7, YELLOW_2:def_5
.= sup (rng (F . j)) by A8, WAYBEL_0:7
.= Sup by YELLOW_2:def_5 ;
hence x in rng (Sups ) by Th14; ::_thesis: verum
end;
then A9: rng (Sups ) c= rng (Sups ) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_rng_(Sups_)_holds_
x_in_rng_(Sups_)
let x be set ; ::_thesis: ( x in rng (Sups ) implies x in rng (Sups ) )
assume x in rng (Sups ) ; ::_thesis: x in rng (Sups )
then consider j being Element of J such that
A10: x = Sup by Th14;
A11: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17;
x = sup (rng (F . j)) by A10, YELLOW_2:def_5
.= sup (rng (F9 . j)) by A11, WAYBEL_0:7
.= Sup by YELLOW_2:def_5 ;
hence x in rng (Sups ) by Th14; ::_thesis: verum
end;
then rng (Sups ) c= rng (Sups ) by TARSKI:def_3;
then ( ex_inf_of rng (Sups ),L9 & rng (Sups ) = rng (Sups ) ) by A9, XBOOLE_0:def_10, YELLOW_0:17;
then inf (rng (Sups )) = inf (rng (Sups )) by A6, YELLOW_0:63;
then A12: Inf = inf (rng (Sups )) by YELLOW_2:def_6;
now__::_thesis:_for_x_being_set_st_x_in_rng_(Infs_)_holds_
x_in_rng_(Infs_)
let x be set ; ::_thesis: ( x in rng (Infs ) implies x in rng (Infs ) )
assume x in rng (Infs ) ; ::_thesis: x in rng (Infs )
then consider f being set such that
A13: f in dom (Frege F) and
A14: x = //\ (((Frege F) . f),S) by Th13;
reconsider f = f as Function by A13;
(Frege F) . f is Function of J, the carrier of S by A13, Th10;
then A15: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def_19;
A16: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17;
then A17: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A15, YELLOW_0:def_18;
x = "/\" ((rng ((Frege F) . f)),S) by A14, YELLOW_2:def_6
.= "/\" ((rng ((Frege F9) . f)),L) by A15, A16, A17, YELLOW_0:63
.= //\ (((Frege F9) . f),L) by YELLOW_2:def_6 ;
hence x in rng (Infs ) by A13, Th13; ::_thesis: verum
end;
then A18: rng (Infs ) c= rng (Infs ) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_rng_(/\\_((Frege_F9),L))_holds_
x_in_rng_(Infs_)
let x be set ; ::_thesis: ( x in rng (/\\ ((Frege F9),L)) implies x in rng (Infs ) )
assume x in rng (/\\ ((Frege F9),L)) ; ::_thesis: x in rng (Infs )
then consider f being set such that
A19: f in dom (Frege F9) and
A20: x = //\ (((Frege F9) . f),L) by Th13;
reconsider f = f as Element of product (doms F9) by A19;
(Frege F) . f is Function of J, the carrier of S by A19, Th10;
then A21: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def_19;
A22: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17;
then A23: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A21, YELLOW_0:def_18;
x = "/\" ((rng ((Frege F9) . f)),L) by A20, YELLOW_2:def_6
.= "/\" ((rng ((Frege F) . f)),S) by A21, A22, A23, YELLOW_0:63
.= //\ (((Frege F) . f),S) by YELLOW_2:def_6 ;
hence x in rng (Infs ) by A19, Th13; ::_thesis: verum
end;
then rng (/\\ ((Frege F9),L)) c= rng (/\\ ((Frege F),S)) by TARSKI:def_3;
then A24: rng (Infs ) = rng (Infs ) by A18, XBOOLE_0:def_10;
for j being Element of J holds rng (F9 . j) is directed
proof
let j be Element of J; ::_thesis: rng (F9 . j) is directed
rng (F . j) is directed by A3;
hence rng (F9 . j) is directed by YELLOW_2:7; ::_thesis: verum
end;
then A25: Inf = Sup by A1, Lm8;
( ex_sup_of rng (/\\ ((Frege F9),L)),L9 & rng (Infs ) is non empty directed Subset of S ) by A2, A3, Th27, YELLOW_0:17;
then sup (rng (Infs )) = sup (rng (Infs )) by A24, WAYBEL_0:7;
then Sup = sup (rng (Infs )) by YELLOW_2:def_5
.= Sup by YELLOW_2:def_5 ;
hence Inf = Sup by A25, A12, YELLOW_2:def_6; ::_thesis: verum
end;
hence S is continuous LATTICE by A2, Lm9; ::_thesis: verum
end;
theorem Th29: :: WAYBEL_5:29
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
let L be complete LATTICE; ::_thesis: 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
let S be non empty Poset; ::_thesis: ( ex g being Function of L,S st
( g is infs-preserving & g is onto ) implies S is complete LATTICE )
given g being Function of L,S such that A1: g is infs-preserving and
A2: g is onto ; ::_thesis: S is complete LATTICE
for A being Subset of S holds ex_inf_of A,S
proof
let A be Subset of S; ::_thesis: ex_inf_of A,S
set Y = g " A;
rng g = the carrier of S by A2, FUNCT_2:def_3;
then A3: A = g .: (g " A) by FUNCT_1:77;
( ex_inf_of g " A,L & g preserves_inf_of g " A ) by A1, WAYBEL_0:def_32, YELLOW_0:17;
hence ex_inf_of A,S by A3, WAYBEL_0:def_30; ::_thesis: verum
end;
then S is non empty complete Poset by YELLOW_2:28;
hence S is complete LATTICE ; ::_thesis: verum
end;
notation
let J, y be set ;
synonym J => y for J --> y;
end;
registration
let J, y be set ;
clusterJ => y -> J -defined total for J -defined Function;
coherence
for b1 being J -defined Function st b1 = J => y holds
b1 is total ;
end;
definition
let A, B, J be set ;
let f be Function of A,B;
:: original: =>
redefine funcJ => f -> ManySortedFunction of J --> A,J --> B;
coherence
J => f is ManySortedFunction of J --> A,J --> B
proof
set JA = J --> A;
set JB = J --> B;
for j being set st j in J holds
(J => f) . j is Function of ((J --> A) . j),((J --> B) . j)
proof
let j be set ; ::_thesis: ( j in J implies (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) )
assume A1: j in J ; ::_thesis: (J => f) . j is Function of ((J --> A) . j),((J --> B) . j)
then ( (J --> A) . j = A & (J --> B) . j = B ) by FUNCOP_1:7;
hence (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) by A1, FUNCOP_1:7; ::_thesis: verum
end;
hence J => f is ManySortedFunction of J --> A,J --> B by PBOOLE:def_15; ::_thesis: verum
end;
end;
theorem Th30: :: WAYBEL_5:30
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
let J be non empty set ; ::_thesis: 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)
let A, B be set ; ::_thesis: 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)
let f be Function of A,B; ::_thesis: for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)
let g be Function of B,A; ::_thesis: ( g * f = id A implies (J => g) ** (J => f) = id (J --> A) )
set F = (J => g) ** (J => f);
dom ((J => g) ** (J => f)) = J by MSUALG_3:2;
then reconsider F = (J => g) ** (J => f) as ManySortedSet of J by PARTFUN1:def_2, RELAT_1:def_18;
assume A1: g * f = id A ; ::_thesis: (J => g) ** (J => f) = id (J --> A)
A2: for j being set st j in J holds
F . j = id ((J --> A) . j)
proof
let j be set ; ::_thesis: ( j in J implies F . j = id ((J --> A) . j) )
assume A3: j in J ; ::_thesis: F . j = id ((J --> A) . j)
then A4: (J --> A) . j = A by FUNCOP_1:7;
( (J => g) . j = g & (J => f) . j = f ) by A3, FUNCOP_1:7;
hence F . j = id ((J --> A) . j) by A1, A3, A4, MSUALG_3:2; ::_thesis: verum
end;
now__::_thesis:_for_j_being_set_st_j_in_J_holds_
F_._j_is_Function_of_((J_-->_A)_._j),((J_-->_A)_._j)
let j be set ; ::_thesis: ( j in J implies F . j is Function of ((J --> A) . j),((J --> A) . j) )
assume j in J ; ::_thesis: F . j is Function of ((J --> A) . j),((J --> A) . j)
then F . j = id ((J --> A) . j) by A2;
hence F . j is Function of ((J --> A) . j),((J --> A) . j) ; ::_thesis: verum
end;
then reconsider F = F as ManySortedFunction of J --> A,J --> A by PBOOLE:def_15;
for j being set st j in J holds
F . j = id ((J --> A) . j) by A2;
hence (J => g) ** (J => f) = id (J --> A) by MSUALG_3:def_1; ::_thesis: verum
end;
theorem Th31: :: WAYBEL_5:31
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
let J, A be non empty set ; ::_thesis: 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
let B be set ; ::_thesis: 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
let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
let F be DoubleIndexedSet of K,A; ::_thesis: for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B
let f be Function of A,B; ::_thesis: (J => f) ** F is DoubleIndexedSet of K,B
set fF = (J => f) ** F;
dom ((J => f) ** F) = J by MSUALG_3:2;
then reconsider fF = (J => f) ** F as ManySortedSet of J by PARTFUN1:def_2, RELAT_1:def_18;
for j being set st j in J holds
fF . j is Function of (K . j),((J --> B) . j)
proof
let j be set ; ::_thesis: ( j in J implies fF . j is Function of (K . j),((J --> B) . j) )
assume A1: j in J ; ::_thesis: fF . j is Function of (K . j),((J --> B) . j)
then reconsider j9 = j as Element of J ;
reconsider Fj = F . j9 as Function of (K . j),A ;
A2: fF . j = ((J => f) . j) * (F . j) by A1, MSUALG_3:2
.= f * Fj by FUNCOP_1:7 ;
(J --> B) . j = B by A1, FUNCOP_1:7;
hence fF . j is Function of (K . j),((J --> B) . j) by A2; ::_thesis: verum
end;
hence (J --> f) ** F is DoubleIndexedSet of K,B by PBOOLE:def_15; ::_thesis: verum
end;
theorem Th32: :: WAYBEL_5:32
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
let J, A, B be non empty set ; ::_thesis: 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
let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,A
for f being Function of A,B holds doms ((J => f) ** F) = doms F
let F be DoubleIndexedSet of K,A; ::_thesis: for f being Function of A,B holds doms ((J => f) ** F) = doms F
let f be Function of A,B; ::_thesis: doms ((J => f) ** F) = doms F
A1: dom (doms ((J => f) ** F)) = dom ((J => f) ** F) by FUNCT_6:59
.= J by MSUALG_3:2 ;
A2: now__::_thesis:_for_x_being_set_st_x_in_J_holds_
(doms_((J_=>_f)_**_F))_._x_=_(doms_F)_._x
let x be set ; ::_thesis: ( x in J implies (doms ((J => f) ** F)) . x = (doms F) . x )
assume A3: x in J ; ::_thesis: (doms ((J => f) ** F)) . x = (doms F) . x
then reconsider j = x as Element of J ;
A4: j in dom F by A3, PARTFUN1:def_2;
A5: ( rng (F . j) c= A & dom f = A ) by FUNCT_2:def_1;
j in dom ((J => f) ** F) by A1, A3, FUNCT_6:59;
then (doms ((J => f) ** F)) . j = dom (((J => f) ** F) . j) by FUNCT_6:22
.= dom (((J => f) . j) * (F . j)) by MSUALG_3:2
.= dom (f * (F . j)) by FUNCOP_1:7
.= dom (F . j) by A5, RELAT_1:27
.= (doms F) . j by A4, FUNCT_6:22 ;
hence (doms ((J => f) ** F)) . x = (doms F) . x ; ::_thesis: verum
end;
dom (doms F) = dom F by FUNCT_6:59
.= J by PARTFUN1:def_2 ;
hence doms ((J => f) ** F) = doms F by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem :: WAYBEL_5:33
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
let L be complete LATTICE; ::_thesis: ( L is continuous implies 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 )
assume A1: L is continuous ; ::_thesis: 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
let S be non empty Poset; ::_thesis: ( ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) implies S is continuous LATTICE )
given g being Function of L,S such that A2: ( g is infs-preserving & g is directed-sups-preserving ) and
A3: g is onto ; ::_thesis: S is continuous LATTICE
reconsider S9 = S as complete LATTICE by A2, A3, Th29;
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
proof
let J be non empty set ; ::_thesis: for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let K be V9() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,S9; ::_thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A4: for j being Element of J holds rng (F . j) is directed ; ::_thesis: Inf = Sup
consider d being Function of S,L such that
A5: [g,d] is Galois and
for t being Element of S holds d . t is_minimum_of g " (uparrow t) by A2, WAYBEL_1:14;
reconsider dF = (J => d) ** F as DoubleIndexedSet of K,L by Th31;
A6: ( ex_inf_of rng (Sups ),L & g preserves_inf_of rng (Sups ) ) by A2, WAYBEL_0:def_32, YELLOW_0:17;
for t being Element of S holds d . t is_minimum_of g " {t} by A3, A5, WAYBEL_1:22;
then A7: g * d = id S by WAYBEL_1:23;
A8: for f being set st f in dom (Frege dF) holds
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
proof
let f be set ; ::_thesis: ( f in dom (Frege dF) implies rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) )
assume A9: f in dom (Frege dF) ; ::_thesis: rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
then reconsider f = f as Element of product (doms dF) ;
A10: dom (Frege dF) = product (doms dF) by PARTFUN1:def_2
.= product (doms F) by Th32
.= dom (Frege F) by PARTFUN1:def_2 ;
A11: dom ((Frege dF) . f) = dom dF by A9, Th8
.= J by PARTFUN1:def_2 ;
A12: now__::_thesis:_for_i_being_set_st_i_in_J_holds_
(g_*_((Frege_dF)_._f))_._i_=_((Frege_F)_._f)_._i
let i be set ; ::_thesis: ( i in J implies (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i )
assume A13: i in J ; ::_thesis: (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i
then reconsider j = i as Element of J ;
A14: j in dom F by A13, PARTFUN1:def_2;
A15: j in dom dF by A13, PARTFUN1:def_2;
then f . j in dom (dF . j) by A9, Th9;
then f . j in dom (((J => d) . j) * (F . j)) by MSUALG_3:2;
then A16: f . j in dom (d * (F . j)) by FUNCOP_1:7;
(g * ((Frege dF) . f)) . j = g . (((Frege dF) . f) . j) by A11, FUNCT_1:13
.= g . ((dF . j) . (f . j)) by A9, A15, Th9
.= g . ((((J => d) . j) * (F . j)) . (f . j)) by MSUALG_3:2
.= g . ((d * (F . j)) . (f . j)) by FUNCOP_1:7
.= (g * (d * (F . j))) . (f . j) by A16, FUNCT_1:13
.= ((id the carrier of S) * (F . j)) . (f . j) by A7, RELAT_1:36
.= (F . j) . (f . j) by FUNCT_2:17
.= ((Frege F) . f) . j by A9, A10, A14, Th9 ;
hence (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i ; ::_thesis: verum
end;
dom g = the carrier of L by FUNCT_2:def_1;
then rng ((Frege dF) . f) c= dom g ;
then A17: dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f) by RELAT_1:27;
dom ((Frege F) . f) = dom F by A9, A10, Th8
.= J by PARTFUN1:def_2 ;
then rng ((Frege F) . f) = rng (g * ((Frege dF) . f)) by A11, A17, A12, FUNCT_1:2
.= g .: (rng ((Frege dF) . f)) by RELAT_1:127 ;
hence rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) ; ::_thesis: verum
end;
A18: rng (Infs ) c= g .: (rng (Infs ))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Infs ) or y in g .: (rng (Infs )) )
assume y in rng (Infs ) ; ::_thesis: y in g .: (rng (Infs ))
then consider f being set such that
A19: f in dom (Frege F) and
A20: y = //\ (((Frege F) . f),S) by Th13;
reconsider f = f as Element of product (doms F) by A19;
reconsider f9 = f as Element of product (doms dF) by Th32;
set X = rng ((Frege dF) . f9);
A21: ( g preserves_inf_of rng ((Frege dF) . f9) & ex_inf_of rng ((Frege dF) . f9),L ) by A2, WAYBEL_0:def_32, YELLOW_0:17;
A22: dom (Frege dF) = product (doms dF) by PARTFUN1:def_2
.= product (doms F) by Th32
.= dom (Frege F) by PARTFUN1:def_2 ;
then rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A19;
then y = "/\" ((g .: (rng ((Frege dF) . f))),S) by A20, YELLOW_2:def_6;
then A23: y = g . (inf (rng ((Frege dF) . f9))) by A21, WAYBEL_0:def_30
.= g . (Inf ) by YELLOW_2:def_6 ;
Inf in rng (Infs ) by A19, A22, Th13;
hence y in g .: (rng (Infs )) by A23, FUNCT_2:35; ::_thesis: verum
end;
A24: g .: (rng (Infs )) c= rng (Infs )
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g .: (rng (Infs )) or y in rng (Infs ) )
assume y in g .: (rng (Infs )) ; ::_thesis: y in rng (Infs )
then consider x being set such that
x in the carrier of L and
A25: x in rng (Infs ) and
A26: y = g . x by FUNCT_2:64;
consider f being set such that
A27: f in dom (Frege dF) and
A28: x = //\ (((Frege dF) . f),L) by A25, Th13;
reconsider f = f as Element of product (doms dF) by A27;
set X = rng ((Frege dF) . f);
( g preserves_inf_of rng ((Frege dF) . f) & ex_inf_of rng ((Frege dF) . f),L ) by A2, WAYBEL_0:def_32, YELLOW_0:17;
then inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f))) by WAYBEL_0:def_30;
then A29: y = inf (g .: (rng ((Frege dF) . f))) by A26, A28, YELLOW_2:def_6;
A30: dom (Frege dF) = product (doms dF) by PARTFUN1:def_2
.= product (doms F) by Th32
.= dom (Frege F) by PARTFUN1:def_2 ;
reconsider f9 = f as Element of product (doms F) by Th32;
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A27;
then y = Inf by A29, YELLOW_2:def_6;
hence y in rng (Infs ) by A27, A30, Th13; ::_thesis: verum
end;
A31: d is monotone by A5, WAYBEL_1:8;
A32: for j being Element of J holds rng (dF . j) is directed
proof
let j be Element of J; ::_thesis: rng (dF . j) is directed
(J => d) . j = d by FUNCOP_1:7;
then A33: rng (dF . j) = rng (d * (F . j)) by MSUALG_3:2
.= d .: (rng (F . j)) by RELAT_1:127 ;
rng (F . j) is directed by A4;
hence rng (dF . j) is directed by A31, A33, YELLOW_2:15; ::_thesis: verum
end;
then ( rng (Infs ) is directed & not rng (Infs ) is empty ) by Th27;
then A34: g preserves_sup_of rng (Infs ) by A2, WAYBEL_0:def_37;
reconsider gdF = (J => g) ** dF as DoubleIndexedSet of K,S ;
A35: ex_sup_of rng (Infs ),L by YELLOW_0:17;
A36: rng (Sups ) c= g .: (rng (Sups ))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Sups ) or y in g .: (rng (Sups )) )
assume y in rng (Sups ) ; ::_thesis: y in g .: (rng (Sups ))
then consider j being Element of J such that
A37: y = Sup by Th14;
gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2
.= g * (dF . j) by FUNCOP_1:7 ;
then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;
then A38: y = sup (g .: (rng (dF . j))) by A37, YELLOW_2:def_5;
rng (dF . j) is directed by A32;
then A39: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def_37;
ex_sup_of rng (dF . j),L by YELLOW_0:17;
then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A39, WAYBEL_0:def_31;
then A40: y = g . (Sup ) by A38, YELLOW_2:def_5;
Sup in rng (Sups ) by Th14;
hence y in g .: (rng (Sups )) by A40, FUNCT_2:35; ::_thesis: verum
end;
A41: g .: (rng (Sups )) c= rng (Sups )
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g .: (rng (Sups )) or y in rng (Sups ) )
assume y in g .: (rng (Sups )) ; ::_thesis: y in rng (Sups )
then consider x being set such that
x in the carrier of L and
A42: x in rng (Sups ) and
A43: y = g . x by FUNCT_2:64;
consider j being Element of J such that
A44: x = Sup by A42, Th14;
rng (dF . j) is directed by A32;
then A45: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def_37;
ex_sup_of rng (dF . j),L by YELLOW_0:17;
then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A45, WAYBEL_0:def_31;
then A46: y = sup (g .: (rng (dF . j))) by A43, A44, YELLOW_2:def_5;
gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2
.= g * (dF . j) by FUNCOP_1:7 ;
then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;
then y = Sup by A46, YELLOW_2:def_5;
hence y in rng (Sups ) by Th14; ::_thesis: verum
end;
F = (id (J --> the carrier of S)) ** F by MSUALG_3:4
.= ((J --> g) ** (J --> d)) ** F by A7, Th30
.= gdF by PBOOLE:140 ;
then Inf = inf (rng (Sups )) by YELLOW_2:def_6
.= inf (g .: (rng (Sups ))) by A36, A41, XBOOLE_0:def_10
.= g . (inf (rng (Sups ))) by A6, WAYBEL_0:def_30
.= g . (Inf ) by YELLOW_2:def_6
.= g . (Sup ) by A1, A32, Lm8
.= g . (sup (rng (Infs ))) by YELLOW_2:def_5
.= sup (g .: (rng (Infs ))) by A34, A35, WAYBEL_0:def_31
.= sup (rng (Infs )) by A24, A18, XBOOLE_0:def_10
.= Sup by YELLOW_2:def_5 ;
hence Inf = Sup ; ::_thesis: verum
end;
hence S is continuous LATTICE by Lm9; ::_thesis: verum
end;