environ
vocabularies HIDDEN, RELAT_1, TARSKI, XBOOLE_0, ORDERS_2, YELLOW_0, FUNCT_1, STRUCT_0, XXREAL_0, SUBSET_1, CAT_1, RELAT_2, WAYBEL_0, SEQM_3, FUNCOP_1, ORDINAL2, BINOP_1, GROUP_6, EQREL_1, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1, REWRITE1, YELLOW_1, WAYBEL_3, NEWTON, CARD_3, PBOOLE, LATTICE3, FUNCT_4, RLVECT_2, ZFMISC_1, LATTICES, PRE_TOPC, RCOMP_1, WAYBEL18, CARD_1, YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, ORDINAL1, NUMBERS, FUNCT_7, FUNCOP_1, STRUCT_0, CARD_3, PRALG_1, FUNCT_4, WELLORD1, ORDERS_2, LATTICE3, PRE_TOPC, TOPS_2, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL18;
definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, T_0TOPSP, WAYBEL25, XBOOLE_0;
theorems YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1, ORDERS_2, YELLOW12, RELAT_1, FUNCT_2, FUNCT_1, ENUMSET1, WAYBEL_3, FUNCOP_1, CARD_3, TARSKI, ZFMISC_1, WELLORD1, QUANTAL1, FUNCT_4, YELLOW_9, WAYBEL20, FUNCT_7, TOPS_2, FUNCT_3, WAYBEL10, WAYBEL15, YELLOW_6, PRALG_1, WAYBEL18, WAYBEL13, WAYBEL21, XBOOLE_0, XBOOLE_1, PARTFUN1, CARD_1;
schemes PBOOLE;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, BORSUK_2, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL10, WAYBEL17, WAYBEL18, RELAT_1;
constructors HIDDEN, TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, MONOID_0, QUANTAL1, ORDERS_3, YELLOW_9, WAYBEL18, WAYBEL20, FUNCT_4;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ORDINAL1, YELLOW_1, YELLOW_2, WAYBEL_1, STRUCT_0;
expansions TARSKI, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_2, WAYBEL_1, T_0TOPSP;
Lm1:
now for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )
let I be non
empty set ;
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )let J be
non-Empty Poset-yielding ManySortedSet of
I;
for X being Subset of (product J) st ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) holds
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )let X be
Subset of
(product J);
( ( for i being Element of I holds ex_sup_of pi (X,i),J . i ) implies ex f being Element of (product J) st
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) ) )deffunc H1(
Element of
I)
-> Element of the
carrier of
(J . $1) =
sup (pi (X,$1));
consider f being
ManySortedSet of
I such that A1:
for
i being
Element of
I holds
f . i = H1(
i)
from PBOOLE:sch 5();
dom f = I
by PARTFUN1:def 2;
then reconsider f =
f as
Element of
(product J) by A2, WAYBEL_3:27;
assume A3:
for
i being
Element of
I holds
ex_sup_of pi (
X,
i),
J . i
;
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )take f =
f;
( ( for i being Element of I holds f . i = sup (pi (X,i)) ) & f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )thus
for
i being
Element of
I holds
f . i = sup (pi (X,i))
by A1;
( f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )thus
f is_>=_than X
for g being Element of (product J) st X is_<=_than g holds
f <= g
let g be
Element of
(product J);
( X is_<=_than g implies f <= g )assume A7:
X is_<=_than g
;
f <= g
hence
f <= g
by WAYBEL_3:28;
verum
end;
Lm2:
now for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )
let I be non
empty set ;
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )let J be
non-Empty Poset-yielding ManySortedSet of
I;
for X being Subset of (product J) st ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) holds
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )let X be
Subset of
(product J);
( ( for i being Element of I holds ex_inf_of pi (X,i),J . i ) implies ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) ) )deffunc H1(
Element of
I)
-> Element of the
carrier of
(J . $1) =
inf (pi (X,$1));
consider f being
ManySortedSet of
I such that A1:
for
i being
Element of
I holds
f . i = H1(
i)
from PBOOLE:sch 5();
dom f = I
by PARTFUN1:def 2;
then reconsider f =
f as
Element of
(product J) by A2, WAYBEL_3:27;
assume A3:
for
i being
Element of
I holds
ex_inf_of pi (
X,
i),
J . i
;
ex f being Element of (product J) st
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )take f =
f;
( ( for i being Element of I holds f . i = inf (pi (X,i)) ) & f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )thus
for
i being
Element of
I holds
f . i = inf (pi (X,i))
by A1;
( f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )thus
f is_<=_than X
for g being Element of (product J) st X is_>=_than g holds
f >= g
let g be
Element of
(product J);
( X is_>=_than g implies f >= g )assume A7:
X is_>=_than g
;
f >= g
hence
f >= g
by WAYBEL_3:28;
verum
end;