let I be non empty set ; for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ( ( for i being Element of I holds J . i is complete continuous LATTICE ) implies product J is continuous )
assume A1:
for i being Element of I holds J . i is complete continuous LATTICE
; product J is continuous
A2:
for i being Element of I holds J . i is complete LATTICE
by A1;
set pJ = product J;
reconsider pJ9 = product J as complete LATTICE by A2, WAYBEL_3:31;
pJ9 is up-complete
;
hence
product J is up-complete
; product J is satisfying_axiom_of_approximation
let x be Element of (product J); WAYBEL_3:def 5 x = "\/" ((waybelow x),(product J))
set swx = sup (waybelow x);
now ( dom x = I & dom (sup (waybelow x)) = I & ( for i being object st i in I holds
x . i = (sup (waybelow x)) . i ) )thus
dom x = I
by WAYBEL_3:27;
( dom (sup (waybelow x)) = I & ( for i being object st i in I holds
x . i = (sup (waybelow x)) . i ) )thus
dom (sup (waybelow x)) = I
by WAYBEL_3:27;
for i being object st i in I holds
x . i = (sup (waybelow x)) . ilet i be
object ;
( i in I implies x . i = (sup (waybelow x)) . i )assume
i in I
;
x . i = (sup (waybelow x)) . ithen reconsider i9 =
i as
Element of
I ;
now for a being object holds
( ( a in pi ((waybelow x),i9) implies a in waybelow (x . i9) ) & ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) )reconsider K =
{i9} as
finite Subset of
I ;
deffunc H1(
Element of
I)
-> Element of the
carrier of
(J . $1) =
Bottom (J . $1);
let a be
object ;
( ( a in pi ((waybelow x),i9) implies a in waybelow (x . i9) ) & ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) )consider g being
ManySortedSet of
I such that A3:
for
i being
Element of
I holds
g . i = H1(
i)
from PBOOLE:sch 5();
set f =
g +* (
i,
a);
A6:
dom g = I
by PARTFUN1:def 2;
then A7:
dom (g +* (i,a)) = I
by FUNCT_7:30;
assume A8:
a in waybelow (x . i9)
;
a in pi ((waybelow x),i9)then reconsider f =
g +* (
i,
a) as
Element of
(product J) by A7, WAYBEL_3:27;
then
f << x
by A2, A9, WAYBEL_3:33;
then A13:
f in waybelow x
;
a = f . i9
by A6, FUNCT_7:31;
hence
a in pi (
(waybelow x),
i9)
by A13, CARD_3:def 6;
verum end; then A14:
pi (
(waybelow x),
i9)
= waybelow (x . i9)
by TARSKI:2;
(
(sup (waybelow x)) . i9 = sup (pi ((waybelow x),i9)) &
J . i9 is
satisfying_axiom_of_approximation )
by A1, A2, WAYBEL_3:32;
hence
x . i = (sup (waybelow x)) . i
by A14;
verum end;
hence
x = "\/" ((waybelow x),(product J))
by FUNCT_1:2; verum