:: Retracts and Inheritance
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: YELLOW16:1
theorem :: YELLOW16:2
theorem :: YELLOW16:3
theorem :: YELLOW16:4
theorem Th5: :: YELLOW16:5
theorem Th6: :: YELLOW16:6
theorem :: YELLOW16:7
canceled;
theorem :: YELLOW16:8
canceled;
theorem Th9: :: YELLOW16:9
:: deftheorem Def1 defines is_a_retraction_of YELLOW16:def 1 :
:: deftheorem Def2 defines is_an_UPS_retraction_of YELLOW16:def 2 :
:: deftheorem Def3 defines is_a_retract_of YELLOW16:def 3 :
:: deftheorem Def4 defines is_an_UPS_retract_of YELLOW16:def 4 :
theorem Th10: :: YELLOW16:10
theorem Th11: :: YELLOW16:11
theorem Th12: :: YELLOW16:12
theorem Th13: :: YELLOW16:13
theorem Th14: :: YELLOW16:14
theorem Th15: :: YELLOW16:15
theorem Th16: :: YELLOW16:16
theorem Th17: :: YELLOW16:17
theorem Th18: :: YELLOW16:18
theorem :: YELLOW16:19
theorem Th20: :: YELLOW16:20
theorem Th21: :: YELLOW16:21
theorem Th22: :: YELLOW16:22
theorem Th23: :: YELLOW16:23
theorem Th24: :: YELLOW16:24
theorem :: YELLOW16:25
theorem :: YELLOW16:26
theorem :: YELLOW16:27
theorem Th28: :: YELLOW16:28
theorem :: YELLOW16:29
theorem :: YELLOW16:30
:: deftheorem Def5 defines Poset-yielding YELLOW16:def 5 :
Lm1:
now
let I be non
empty set ;
:: thesis: 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;
:: thesis: 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);
:: thesis: ( ( 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();
A2:
dom f = I
by PBOOLE:def 3;
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
;
:: thesis: 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;
:: thesis: ( ( 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;
:: thesis: ( f is_>=_than X & ( for g being Element of (product J) st X is_<=_than g holds
f <= g ) )thus
f is_>=_than X
:: thesis: for g being Element of (product J) st X is_<=_than g holds
f <= g
let g be
Element of
(product J);
:: thesis: ( X is_<=_than g implies f <= g )assume A5:
X is_<=_than g
;
:: thesis: f <= g
hence
f <= g
by WAYBEL_3:28;
:: thesis: verum
end;
Lm2:
now
let I be non
empty set ;
:: thesis: 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;
:: thesis: 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);
:: thesis: ( ( 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();
A2:
dom f = I
by PBOOLE:def 3;
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
;
:: thesis: 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;
:: thesis: ( ( 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;
:: thesis: ( f is_<=_than X & ( for g being Element of (product J) st X is_>=_than g holds
f >= g ) )thus
f is_<=_than X
:: thesis: for g being Element of (product J) st X is_>=_than g holds
f >= g
let g be
Element of
(product J);
:: thesis: ( X is_>=_than g implies f >= g )assume A5:
X is_>=_than g
;
:: thesis: f >= g
hence
f >= g
by WAYBEL_3:28;
:: thesis: verum
end;
theorem Th31: :: YELLOW16:31
theorem Th32: :: YELLOW16:32
theorem Th33: :: YELLOW16:33
theorem Th34: :: YELLOW16:34
theorem Th35: :: YELLOW16:35
theorem Th36: :: YELLOW16:36
theorem Th37: :: YELLOW16:37
theorem Th38: :: YELLOW16:38
theorem Th39: :: YELLOW16:39
theorem :: YELLOW16:40
theorem Th41: :: YELLOW16:41
:: deftheorem Def6 defines inherits_sup_of YELLOW16:def 6 :
:: deftheorem Def7 defines inherits_inf_of YELLOW16:def 7 :
theorem Th42: :: YELLOW16:42
theorem :: YELLOW16:43
theorem :: YELLOW16:44
theorem Th45: :: YELLOW16:45
theorem Th46: :: YELLOW16:46
theorem :: YELLOW16:47
theorem Th48: :: YELLOW16:48
theorem :: YELLOW16:49
theorem :: YELLOW16:50
theorem :: YELLOW16:51
theorem :: YELLOW16:52
theorem :: YELLOW16:53
theorem Th54: :: YELLOW16:54
theorem Th55: :: YELLOW16:55
theorem Th56: :: YELLOW16:56
theorem Th57: :: YELLOW16:57
theorem Th58: :: YELLOW16:58
theorem :: YELLOW16:59