:: Kuratowski - Zorn Lemma :: by Wojciech A. Trybulec and Grzegorz Bancerek :: :: Received September 19, 1989 :: Copyright (c) 1990-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 STRUCT_0, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, ORDERS_1, SUBSET_1, XXREAL_0, ARYTM_3, TREES_2, TARSKI, WELLORD1, FUNCT_1, ZFMISC_1, ORDERS_2, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, CARD_1, WELLORD1, DOMAIN_1, STRUCT_0, ORDERS_1; constructors RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_1, PRE_TOPC, RELSET_1, SETFAM_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, CARD_1, RELAT_2; requirements BOOLE, SUBSET, NUMERALS; begin :: Original ORDERS_1 reserve X,Y,x,y for set; definition struct(1-sorted) RelStr (# carrier -> set, InternalRel -> Relation of the carrier #); end; registration let X be non empty set; let R be Relation of X; cluster RelStr(#X,R#) -> non empty; end; definition let A be RelStr; attr A is total means :: ORDERS_2:def 1 the InternalRel of A is total; attr A is reflexive means :: ORDERS_2:def 2 the InternalRel of A is_reflexive_in the carrier of A; attr A is transitive means :: ORDERS_2:def 3 the InternalRel of A is_transitive_in the carrier of A; attr A is antisymmetric means :: ORDERS_2:def 4 the InternalRel of A is_antisymmetric_in the carrier of A; end; registration cluster reflexive transitive antisymmetric strict total 1-element for RelStr; end; registration cluster reflexive -> total for RelStr; end; definition mode Poset is reflexive transitive antisymmetric RelStr; end; registration let A be total RelStr; cluster the InternalRel of A -> total; end; registration let A be reflexive RelStr; cluster the InternalRel of A -> reflexive; end; registration let A be total antisymmetric RelStr; cluster the InternalRel of A -> antisymmetric; end; registration let A be total transitive RelStr; cluster the InternalRel of A -> transitive; end; registration let X be set; let O be total reflexive Relation of X; cluster RelStr(#X,O#) -> reflexive; end; registration let X be set; let O be total transitive Relation of X; cluster RelStr(#X,O#) -> transitive; end; registration let X be set; let O be total antisymmetric Relation of X; cluster RelStr(#X,O#) -> antisymmetric; end; reserve A for non empty Poset; reserve a,a1,a2,a3,b,c for Element of A; reserve S,T for Subset of A; definition let A be RelStr; let a1,a2 be Element of A; pred a1 <= a2 means :: ORDERS_2:def 5 [a1,a2] in the InternalRel of A; end; notation let A be RelStr; let a1,a2 be Element of A; synonym a2 >= a1 for a1 <= a2; end; definition let A be RelStr; let a1,a2 be Element of A; pred a1 < a2 means :: ORDERS_2:def 6 a1 <= a2 & a1 <> a2; irreflexivity; end; notation let A be RelStr; let a1,a2 be Element of A; synonym a2 > a1 for a1 < a2; end; theorem :: ORDERS_2:1 for A being reflexive non empty RelStr, a being Element of A holds a <= a; definition let A be reflexive non empty RelStr; let a1,a2 be Element of A; redefine pred a1 <= a2; reflexivity; end; theorem :: ORDERS_2:2 for A being antisymmetric RelStr, a1,a2 being Element of A st a1 <= a2 & a2 <= a1 holds a1 = a2; theorem :: ORDERS_2:3 for A being transitive RelStr, a1,a2,a3 being Element of A holds a1 <= a2 & a2 <= a3 implies a1 <= a3; theorem :: ORDERS_2:4 for A being antisymmetric RelStr, a1,a2 being Element of A holds not(a1 < a2 & a2 < a1); theorem :: ORDERS_2:5 for A being transitive antisymmetric RelStr for a1,a2,a3 being Element of A holds a1 < a2 & a2 < a3 implies a1 < a3; theorem :: ORDERS_2:6 for A being antisymmetric RelStr, a1,a2 being Element of A holds a1 <= a2 implies not a2 < a1; theorem :: ORDERS_2:7 for A being transitive antisymmetric RelStr for a1,a2,a3 being Element of A holds a1 < a2 & a2 <= a3 or a1 <= a2 & a2 < a3 implies a1 < a3; :: :: Chains. :: definition let A be RelStr; let IT be Subset of A; attr IT is strongly_connected means :: ORDERS_2:def 7 the InternalRel of A is_strongly_connected_in IT; end; registration let A be RelStr; cluster empty -> strongly_connected for Subset of A; end; registration let A be RelStr; cluster strongly_connected for Subset of A; end; definition let A be RelStr; mode Chain of A is strongly_connected Subset of A; end; theorem :: ORDERS_2:8 for A being non empty reflexive RelStr for a being Element of A holds {a} is Chain of A; theorem :: ORDERS_2:9 for A being non empty reflexive RelStr, a1,a2 being Element of A holds {a1,a2} is Chain of A iff a1 <= a2 or a2 <= a1; theorem :: ORDERS_2:10 for A being RelStr, C being Chain of A, S being Subset of A holds S c= C implies S is Chain of A; theorem :: ORDERS_2:11 for A being reflexive RelStr, a1,a2 being Element of A holds (ex C being Chain of A st a1 in C & a2 in C) iff a1 <= a2 or a2 <= a1; theorem :: ORDERS_2:12 for A being reflexive antisymmetric RelStr, a1,a2 being Element of A holds (ex C being Chain of A st a1 in C & a2 in C) iff (a1 < a2 iff not a2 <= a1); theorem :: ORDERS_2:13 for A being RelStr, T being Subset of A holds the InternalRel of A well_orders T implies T is Chain of A; :: :: Upper and lower cones. :: definition let A; let S; func UpperCone(S) -> Subset of A equals :: ORDERS_2:def 8 {a1 : for a2 st a2 in S holds a2 < a1}; end; definition let A; let S; func LowerCone(S) -> Subset of A equals :: ORDERS_2:def 9 {a1 : for a2 st a2 in S holds a1 < a2}; end; theorem :: ORDERS_2:14 UpperCone({}(A)) = the carrier of A; theorem :: ORDERS_2:15 UpperCone([#](A)) = {}; theorem :: ORDERS_2:16 LowerCone({}(A)) = the carrier of A; theorem :: ORDERS_2:17 LowerCone([#](A)) = {}; theorem :: ORDERS_2:18 a in S implies not a in UpperCone(S); theorem :: ORDERS_2:19 not a in UpperCone{a}; theorem :: ORDERS_2:20 a in S implies not a in LowerCone(S); theorem :: ORDERS_2:21 not a in LowerCone{a}; theorem :: ORDERS_2:22 c < a iff a in UpperCone{c}; theorem :: ORDERS_2:23 a < c iff a in LowerCone{c}; :: :: Initial segments. :: definition let A; let S; let a; func InitSegm(S,a) -> Subset of A equals :: ORDERS_2:def 10 LowerCone{a} /\ S; end; definition let A; let S; mode Initial_Segm of S -> Subset of A means :: ORDERS_2:def 11 ex a st a in S & it = InitSegm(S,a) if S <> {} otherwise it = {}; end; theorem :: ORDERS_2:24 a in InitSegm(S,b) iff a < b & a in S; theorem :: ORDERS_2:25 InitSegm({}(A),a) = {}; theorem :: ORDERS_2:26 not a in InitSegm(S,a); theorem :: ORDERS_2:27 a1 < a2 implies InitSegm(S,a1) c= InitSegm(S,a2); theorem :: ORDERS_2:28 S c= T implies InitSegm(S,a) c= InitSegm(T,a); theorem :: ORDERS_2:29 for I being Initial_Segm of S holds I c= S; theorem :: ORDERS_2:30 S <> {} iff not S is Initial_Segm of S; theorem :: ORDERS_2:31 S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S; theorem :: ORDERS_2:32 a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T; theorem :: ORDERS_2:33 a in S & S is Initial_Segm of T implies InitSegm(S,a) = InitSegm (T,a); theorem :: ORDERS_2:34 S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T; theorem :: ORDERS_2:35 S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T ; :: :: Chains of choice function of BOOL of partially ordered sets. :: reserve f for Choice_Function of BOOL(the carrier of A); definition let A; let f; mode Chain of f -> Chain of A means :: ORDERS_2:def 12 it <> {} & the InternalRel of A well_orders it & for a st a in it holds f.UpperCone(InitSegm(it,a)) = a; end; reserve fC,fC1,fC2 for Chain of f; theorem :: ORDERS_2:36 {f.(the carrier of A)} is Chain of f; theorem :: ORDERS_2:37 f.(the carrier of A) in fC; theorem :: ORDERS_2:38 a in fC & b = f.(the carrier of A) implies b <= a; theorem :: ORDERS_2:39 a = f.(the carrier of A) implies InitSegm(fC,a) = {}; theorem :: ORDERS_2:40 fC1 meets fC2; theorem :: ORDERS_2:41 fC1 <> fC2 implies (fC1 is Initial_Segm of fC2 iff not fC2 is Initial_Segm of fC1); theorem :: ORDERS_2:42 fC1 c< fC2 iff fC1 is Initial_Segm of fC2; definition let A; let f; func Chains f -> set means :: ORDERS_2:def 13 x in it iff x is Chain of f; end; registration let A; let f; cluster Chains f -> non empty; end; theorem :: ORDERS_2:43 union(Chains(f)) <> {}; theorem :: ORDERS_2:44 fC <> union(Chains(f)) & S = union(Chains(f)) implies fC is Initial_Segm of S ; theorem :: ORDERS_2:45 union(Chains(f)) is Chain of f; begin :: From original ORDERS_2 reserve R for Relation, A for non empty Poset, C for Chain of A, S for Subset of A, a,a1,a2,b,c1,c2 for Element of A; :: :: Orders. :: theorem :: ORDERS_2:46 field((the InternalRel of A) |_2 S) = S; theorem :: ORDERS_2:47 (the InternalRel of A) |_2 S is being_linear-order implies S is Chain of A; theorem :: ORDERS_2:48 (the InternalRel of A) |_2 C is being_linear-order; theorem :: ORDERS_2:49 the InternalRel of A linearly_orders S implies S is Chain of A; theorem :: ORDERS_2:50 the InternalRel of A linearly_orders C; theorem :: ORDERS_2:51 a is_minimal_in the InternalRel of A iff for b holds not b < a; theorem :: ORDERS_2:52 a is_maximal_in the InternalRel of A iff for b holds not a < b; theorem :: ORDERS_2:53 a is_superior_of the InternalRel of A iff for b st a <> b holds b < a; theorem :: ORDERS_2:54 a is_inferior_of the InternalRel of A iff for b st a <> b holds a < b; :: :: Kuratowski - Zorn Lemma. :: theorem :: ORDERS_2:55 (for C ex a st for b st b in C holds b <= a) implies ex a st for b holds not a < b; theorem :: ORDERS_2:56 (for C ex a st for b st b in C holds a <= b) implies ex a st for b holds not b < a; :: from YELLOW14, 2009.07.26, A.T. registration cluster strict empty for RelStr; end;