begin
theorem
theorem
theorem
theorem
theorem Th5:
theorem Th6:
theorem
canceled;
theorem
canceled;
theorem Th9:
:: deftheorem Def1 defines is_a_retraction_of YELLOW16:def 1 :
for S, T being non empty Poset
for f being Function holds
( f is_a_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & f | the carrier of S = id S & S is full directed-sups-inheriting SubRelStr of T ) );
:: deftheorem Def2 defines is_an_UPS_retraction_of YELLOW16:def 2 :
for S, T being non empty Poset
for f being Function holds
( f is_an_UPS_retraction_of T,S iff ( f is directed-sups-preserving Function of T,S & ex g being directed-sups-preserving Function of S,T st f * g = id S ) );
:: deftheorem Def3 defines is_a_retract_of YELLOW16:def 3 :
for S, T being non empty Poset holds
( S is_a_retract_of T iff ex f being Function of T,S st f is_a_retraction_of T,S );
:: deftheorem Def4 defines is_an_UPS_retract_of YELLOW16:def 4 :
for S, T being non empty Poset holds
( S is_an_UPS_retract_of T iff ex f being Function of T,S st f is_an_UPS_retraction_of T,S );
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem Th28:
theorem
theorem
begin
:: deftheorem Def5 defines Poset-yielding YELLOW16:def 5 :
for R being Relation holds
( R is Poset-yielding iff for x being set st x in rng R holds
x is Poset );
Lm1:
now
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 4;
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
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 4;
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;
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
begin
:: deftheorem Def6 defines inherits_sup_of YELLOW16:def 6 :
for S, T being non empty RelStr
for X being set holds
( S inherits_sup_of X,T iff ( ex_sup_of X,T implies "\/" (X,T) in the carrier of S ) );
:: deftheorem Def7 defines inherits_inf_of YELLOW16:def 7 :
for S, T being non empty RelStr
for X being set holds
( S inherits_inf_of X,T iff ( ex_inf_of X,T implies "/\" (X,T) in the carrier of S ) );
theorem Th42:
theorem
theorem
theorem Th45:
begin
theorem Th46:
theorem
theorem Th48:
theorem
theorem
theorem
theorem
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem