:: Morphisms Into Chains, Part {I}
:: by Artur Korni{\l}owicz
::
:: Received February 6, 2003
:: Copyright (c) 2003-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ORDERS_2, WAYBEL_4,
RELAT_1, RELAT_2, LATTICE3, LATTICES, FUNCT_1, YELLOW_1, LATTICE7,
WAYBEL_0, SEQM_3, XXREAL_0, TARSKI, ARYTM_3, GROUP_4, ORDERS_1, WELLORD2,
WELLORD1, YELLOW_0, EQREL_1, REWRITE1, WAYBEL_1, ORDINAL2, NUMBERS,
CARD_1, NAT_1, WAYBEL35, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1,
FUNCT_7, STRUCT_0, WELLORD1, ORDERS_2, ORDERS_1, LATTICE3, YELLOW_0,
YELLOW_1, ALG_1, WAYBEL_0, WAYBEL_1, WAYBEL_4, LATTICE7;
constructors WELLORD1, NAT_1, REALSET1, ORDERS_3, WAYBEL_1, WAYBEL_4,
LATTICE7, RELSET_1, NUMBERS, FUNCT_7;
registrations SUBSET_1, ORDINAL1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_4, ZFMISC_1, CARD_1, XCMPLX_0,
NAT_1, XXREAL_0;
requirements SUBSET, BOOLE, NUMERALS;
begin
begin :: Main part
registration
let L be RelStr;
cluster auxiliary(i) for Relation of L;
end;
registration
let L be transitive RelStr;
cluster auxiliary(i) auxiliary(ii) for Relation of L;
end;
registration
let L be with_suprema antisymmetric RelStr;
cluster auxiliary(iii) for Relation of L;
end;
registration
let L be non empty lower-bounded antisymmetric RelStr;
cluster auxiliary(iv) for Relation of L;
end;
:: Definition 2.1, p. 203
definition
let L be non empty RelStr, R be Relation of L;
attr R is extra-order means
:: WAYBEL35:def 1
R is auxiliary(i) auxiliary(ii) auxiliary(iv);
end;
registration
let L be non empty RelStr;
cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for
Relation of
L;
cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for
Relation of
L;
end;
registration
let L be non empty RelStr;
cluster extra-order auxiliary(iii) -> auxiliary for Relation of L;
cluster auxiliary -> extra-order for Relation of L;
end;
registration
let L be lower-bounded antisymmetric transitive non empty RelStr;
cluster extra-order for Relation of L;
end;
definition
let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;
func R-LowerMap -> Function of L, InclPoset LOWER L means
:: WAYBEL35:def 2
for x being Element of L holds it.x = R-below x;
end;
registration
let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;
cluster R-LowerMap -> monotone;
end;
definition
let L be 1-sorted, R be Relation of the carrier of L;
mode strict_chain of R -> Subset of L means
:: WAYBEL35:def 3
for x, y being set st x
in it & y in it holds [x,y] in R or x = y or [y,x] in R;
end;
theorem :: WAYBEL35:1
for L being 1-sorted, C being trivial Subset of L, R being
Relation of the carrier of L holds C is strict_chain of R;
registration
let L be non empty 1-sorted, R be Relation of the carrier of L;
cluster 1-element for strict_chain of R;
end;
theorem :: WAYBEL35:2
for L being antisymmetric RelStr, R being auxiliary(i) (Relation
of L), C being strict_chain of R, x, y being Element of L st x in C & y in C &
x < y holds [x,y] in R;
theorem :: WAYBEL35:3
for L being antisymmetric RelStr, R being auxiliary(i) (Relation of L)
, x, y being Element of L st [x,y] in R & [y,x] in R holds x = y;
theorem :: WAYBEL35:4
for L being non empty lower-bounded antisymmetric RelStr, x being
Element of L, R being auxiliary(iv) Relation of L holds {Bottom L, x} is
strict_chain of R;
theorem :: WAYBEL35:5
for L being non empty lower-bounded antisymmetric RelStr, R being
auxiliary(iv) (Relation of L), C being strict_chain of R holds C \/ {Bottom L}
is strict_chain of R;
definition
let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
R;
attr C is maximal means
:: WAYBEL35:def 4
for D being strict_chain of R st C c= D holds C = D;
end;
definition
let L be 1-sorted, R be (Relation of the carrier of L), C be set;
func Strict_Chains (R,C) -> set means
:: WAYBEL35:def 5
for x being set holds x in it iff x is strict_chain of R & C c= x;
end;
registration
let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
R;
cluster Strict_Chains (R,C) -> non empty;
end;
notation
let R be Relation, X be set;
synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R;
end;
:: Lemma 2.2, p. 203
theorem :: WAYBEL35:6
for L being 1-sorted, R being (Relation of the carrier of L), C being
strict_chain of R holds Strict_Chains (R,C) is_inductive_wrt RelIncl
Strict_Chains (R,C) & ex D being set st D is_maximal_in RelIncl Strict_Chains (
R,C) & C c= D;
:: Lemma 2.3 (ii), p. 203
:: It is a trivial consequence of YELLOW_0:65
:: Maybe to cancel
theorem :: WAYBEL35:7
for L being non empty transitive RelStr, C being non empty
Subset of L, X being Subset of C st ex_sup_of X,L & "\/"(X,L) in C holds
ex_sup_of X,subrelstr C & "\/"(X,L) = "\/"(X,subrelstr C);
:: Lemma 2.3, p. 203
theorem :: WAYBEL35:8
for L being non empty Poset, R being auxiliary(i) auxiliary(ii)
(Relation of L), C being non empty strict_chain of R, X being Subset of C st
ex_sup_of X,L & C is maximal holds ex_sup_of X,subrelstr C;
:: Lemma 2.3 (i), (iii), p. 203
theorem :: WAYBEL35:9
for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (
Relation of L), C being non empty strict_chain of R, X being Subset of C st
ex_inf_of (uparrow "\/"(X,L)) /\ C,L & ex_sup_of X,L & C is maximal holds "\/"(
X,subrelstr C) = "/\"((uparrow "\/"(X,L)) /\ C,L) & (not "\/"(X,L) in C implies
"\/"(X,L) < "/\"((uparrow "\/"(X,L)) /\ C,L));
:: Proposition 2.4, p. 204
theorem :: WAYBEL35:10
for L being complete non empty Poset, R being auxiliary(i)
auxiliary(ii) (Relation of L), C being non empty strict_chain of R st C is
maximal holds subrelstr C is complete;
:: Proposition 2.5 (i), p. 204
theorem :: WAYBEL35:11
for L being non empty lower-bounded antisymmetric RelStr, R being
auxiliary(iv) (Relation of L), C being strict_chain of R st C is maximal holds
Bottom L in C;
:: Proposition 2.5 (ii), p. 204
theorem :: WAYBEL35:12
for L being non empty upper-bounded Poset, R being auxiliary(ii) (
Relation of L), C being strict_chain of R, m being Element of L st C is maximal
& m is_maximum_of C & [m,Top L] in R holds [Top L,Top L] in R & m = Top L;
:: Definition (SI_C) p. 204
definition
let L be RelStr, C be set, R be Relation of the carrier of L;
pred R satisfies_SIC_on C means
:: WAYBEL35:def 6
for x, z being Element of L holds x
in C & z in C & [x,z] in R & x <> z implies ex y being Element of L st y in C &
[x,y] in R & [y,z] in R & x <> y;
end;
definition
let L be RelStr, R be (Relation of the carrier of L), C be strict_chain of R;
attr C is satisfying_SIC means
:: WAYBEL35:def 7
R satisfies_SIC_on C;
end;
theorem :: WAYBEL35:13
for L being RelStr, C being set, R being auxiliary(i) (Relation
of L) st R satisfies_SIC_on C holds for x, z being Element of L holds x in C &
z in C & [x,z] in R & x <> z implies ex y being Element of L st y in C & [x,y]
in R & [y,z] in R & x < y;
registration
let L be RelStr, R be Relation of the carrier of L;
cluster trivial -> satisfying_SIC for strict_chain of R;
end;
registration
let L be non empty RelStr, R be Relation of the carrier of L;
cluster 1-element for strict_chain of R;
end;
:: Proposition 2.5 (iii), p. 204
theorem :: WAYBEL35:14
for L being lower-bounded with_suprema Poset, R being auxiliary(i)
auxiliary(ii) (Relation of L), C being strict_chain of R st C is maximal & R is
satisfying_SI holds R satisfies_SIC_on C;
definition
let R be Relation, C be set, y be object;
func SetBelow (R,C,y) -> set equals
:: WAYBEL35:def 8
( R"{y} ) /\ C;
end;
theorem :: WAYBEL35:15
for R being Relation, C, x, y being set holds x in SetBelow (R,C
,y) iff [x,y] in R & x in C;
definition
let L be 1-sorted, R be (Relation of the carrier of L),
C be set, y be object;
redefine func SetBelow (R,C,y) -> Subset of L;
end;
theorem :: WAYBEL35:16
for L being RelStr, R being auxiliary(i) (Relation of L), C
being set, y being Element of L holds SetBelow (R,C,y) is_<=_than y;
theorem :: WAYBEL35:17
for L being reflexive transitive RelStr, R being auxiliary(ii) (
Relation of L), C being Subset of L, x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y);
theorem :: WAYBEL35:18
for L being RelStr, R being auxiliary(i) (Relation of L), C
being set, x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,
C,x),L holds x = sup SetBelow (R,C,x);
definition
let L be RelStr, C be Subset of L;
attr C is sup-closed means
:: WAYBEL35:def 9
for X being Subset of C st ex_sup_of X,L
holds "\/"(X,L) = "\/"(X,subrelstr C);
end;
:: Lemma 2.6, p. 205
theorem :: WAYBEL35:19
for L being complete non empty Poset, R being extra-order (
Relation of L), C being satisfying_SIC strict_chain of R, p, q being Element of
L st p in C & q in C & p < q ex y being Element of L st p < y & [y,q] in R & y
= sup SetBelow (R,C,y);
:: Lemma 2.7, p. 205, 1 => 2
theorem :: WAYBEL35:20
for L being lower-bounded non empty Poset, R being extra-order (
Relation of L), C being non empty strict_chain of R st C is sup-closed & (for c
being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L) & R
satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup
SetBelow (R,C,c);
:: Lemma 2.7, p. 205, 2 => 1
theorem :: WAYBEL35:21
for L being non empty reflexive antisymmetric RelStr, R being
auxiliary(i) (Relation of L), C being strict_chain of R st (for c being Element
of L st c in C holds ex_sup_of SetBelow (R,C,c),L & c = sup SetBelow (R,C,c))
holds R satisfies_SIC_on C;
definition
let L be non empty RelStr, R be (Relation of the carrier of L), C be set;
func SupBelow (R,C) -> set means
:: WAYBEL35:def 10
for y being set holds y in it iff y = sup SetBelow (R,C,y);
end;
definition
let L be non empty RelStr, R be (Relation of the carrier of L), C be set;
redefine func SupBelow (R,C) -> Subset of L;
end;
:: Lemma 2.8, (i) a), p. 205
theorem :: WAYBEL35:22
for L being non empty reflexive transitive RelStr, R being
auxiliary(i) auxiliary(ii) (Relation of L), C being strict_chain of R st (for c
being Element of L holds ex_sup_of SetBelow (R,C,c),L) holds SupBelow (R,C) is
strict_chain of R;
:: Lemma 2.8, (i) b), p. 205
theorem :: WAYBEL35:23
for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (
Relation of L), C being Subset of L st (for c being Element of L holds
ex_sup_of SetBelow (R,C,c),L) holds SupBelow (R,C) is sup-closed;
theorem :: WAYBEL35:24
for L being complete non empty Poset, R being extra-order (
Relation of L), C being satisfying_SIC strict_chain of R, d being Element of L
st d in SupBelow (R,C) holds d = "\/"({b where b is Element of L: b in SupBelow
(R,C) & [b,d] in R},L);
:: Lemma 2.8, (ii), p. 205
theorem :: WAYBEL35:25
for L being complete non empty Poset, R being extra-order (Relation of
L), C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow
(R,C);
:: Lemma 2.8, (iii), p. 205
theorem :: WAYBEL35:26
for L being complete non empty Poset, R being extra-order (Relation of
L), C being satisfying_SIC strict_chain of R, a, b being Element of L st a in C
& b in C & a < b ex d being Element of L st d in SupBelow (R,C) & a < d & [d,b]
in R;