:: Kuratowski - Zorn Lemma
:: by Wojciech A. Trybulec and Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2016 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;