let L be complete LATTICE; ( ( for J being non empty set st J in the_universe_of the carrier of L holds
for K being non-empty 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 non-empty 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
; L is continuous
now 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;
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
( 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
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
for
i being
object st
i in J holds
not
K . i is
empty
then reconsider K =
K as
non-empty ManySortedSet of
J by PBOOLE:def 13;
deffunc H1(
object )
-> Element of
bool [:(K . $1),(K . $1):] =
id (K . $1);
ex
F being
Function st
(
dom F = J & ( for
j being
object 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
object 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
object st
j in dom F holds
F . j is
Function
then reconsider F =
F as
ManySortedFunction of
J by FUNCOP_1:def 6;
for
j being
object st
j in J holds
F . j is
Function of
(K . j),
((J --> the carrier of L) . j)
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
A16:
for
j being
Element of
J holds
rng (F . j) = j
A20:
for
j being
Element of
J holds
rng (F . j) is
directed
for
f being
Function st
f in dom (Frege F) holds
//\ (
((Frege F) . f),
L)
<= sup (waybelow x)
proof
let f be
Function;
( f in dom (Frege F) implies //\ (((Frege F) . f),L) <= sup (waybelow x) )
assume A21:
f in dom (Frege F)
;
//\ (((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
A23:
dom f =
dom F
by A21, Th8
.=
J
by PARTFUN1:def 2
;
then
rng f c= the
carrier of
L
;
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;
( x <= sup D implies ex d being Element of L st
( d in D & //\ (((Frege F) . f),L) <= d ) )
assume
x <= sup D
;
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
;
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;
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;
verum
end; then A32:
Sup <= sup (waybelow x)
by Th15;
x is_<=_than rng (Sups )
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;
verum end;
then
( L is up-complete & L is satisfying_axiom_of_approximation )
by WAYBEL_3:def 5;
hence
L is continuous
; verum