begin
This theory file contains properties of finite sets related to order relations. Part of this is similar to what is done in Finite_ZF_1 except that the development is based on the notion of finite powerset defined in Finite_ZF rather the one defined in standard Isabelle Finite theory.
Finite vs. bounded sets
The goal of this section is to show that finite sets are bounded and have maxima and minima.
For total and transitive relations nonempty finite set has a maximum.
theorem fin_has_max:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( B \in \text{FinPow}(X) \) and A4: \( B \neq 0 \)
shows \( \text{HasAmaximum}(r,B) \)proof have \( \emptyset =\emptyset \vee \text{HasAmaximum}(r,\emptyset ) \)
moreover
qed
have \( \forall A \in \text{FinPow}(X).\ A=\emptyset \vee \text{HasAmaximum}(r,A) \longrightarrow \)
\( (\forall x\in X.\ (A \cup \{x\}) = \emptyset \vee \text{HasAmaximum}(r,A \cup \{x\})) \)proof
moreover {
}
fix \( A \)
assume \( A \in \text{FinPow}(X) \), \( A = \emptyset \vee \text{HasAmaximum}(r,A) \)
have \( \forall x\in X.\ (A \cup \{x\}) = \emptyset \vee \text{HasAmaximum}(r,A \cup \{x\}) \)proof
{
}
fix \( x \)
assume \( x\in X \)
note \( A = \emptyset \vee \text{HasAmaximum}(r,A) \)
moreover {
}
moreover {
}
ultimately have \( A \cup \{x\} = \emptyset \vee \text{HasAmaximum}(r,A \cup \{x\}) \)
assume \( A = \emptyset \)
then have \( A\cup \{x\} = \{x\} \)
from A1 have \( \text{refl}(X,r) \) using total_is_refl
with \( x\in X \), \( A\cup \{x\} = \{x\} \) have \( \text{HasAmaximum}(r,A\cup \{x\}) \) using Order_ZF_4_L8
assume \( \text{HasAmaximum}(r,A) \)
with A1, A2, \( A \in \text{FinPow}(X) \), \( x\in X \) have \( \text{HasAmaximum}(r,A\cup \{x\}) \) using FinPow_def, Order_ZF_4_L9
thus \( \forall x\in X.\ (A \cup \{x\}) = 0 \vee \text{HasAmaximum}(r,A \cup \{x\}) \)
qed
thus \( thesis \)
qed
note A3
ultimately have \( B = \emptyset \vee \text{HasAmaximum}(r,B) \) by (rule FinPow_induct )
with A4 show \( \text{HasAmaximum}(r,B) \)
For total and transitive relations nonempty finite set has a minimum.
theorem fin_has_min:
assumes \( r \text{ is total on } X \), \( \text{trans}(r) \), \( B \in \text{FinPow}(X) \), \( B\neq 0 \)
shows \( \text{HasAminimum}(r,B) \)proof from assms(1) have \( \text{refl}(X,r) \) using total_is_refl
with assms(1,2,3) have \( \emptyset =\emptyset \vee \text{HasAminimum}(r,\emptyset ) \) and \( \forall A \in \text{FinPow}(X).\ A=\emptyset \vee \text{HasAminimum}(r,A) \longrightarrow \)
\( (\forall x\in X.\ (A \cup \{x\}) = \emptyset \vee \text{HasAminimum}(r,A \cup \{x\})) \) and \( B \in \text{FinPow}(X) \) using Order_ZF_4_L8(2), Order_ZF_4_L10 unfolding FinPow_def
then have \( B = \emptyset \vee \text{HasAminimum}(r,B) \) by (rule FinPow_induct )
with assms(4) show \( \text{HasAminimum}(r,B) \)
qed
For linearly ordered nonempty finite sets the maximum is in the set and indeed it is the greatest element of the set.
lemma linord_min_max_props:
assumes \( \text{IsLinOrder}(X,r) \), \( A \in \text{FinPow}(X) \), \( A\neq \emptyset \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall a\in A.\ \langle a, \text{Maximum}(r,A)\rangle \in r \), \( \text{Minimum}(r,A) \in A \), \( \forall a\in A.\ \langle \text{Minimum}(r,A),a\rangle \in r \), \( \text{Maximum}(r,A) \in X \), \( \text{Minimum}(r,A) \in X \)proof from assms show \( \text{Maximum}(r,A) \in A \), \( \forall a\in A.\ \langle a, \text{Maximum}(r,A)\rangle \in r \) and \( \text{Minimum}(r,A) \in A \), \( \forall a\in A.\ \langle \text{Minimum}(r,A),a\rangle \in r \) using fin_has_max, fin_has_min, Order_ZF_4_L3, Order_ZF_4_L4 unfolding IsLinOrder_def
with assms(2,3) show \( \text{Maximum}(r,A) \in X \) and \( \text{Minimum}(r,A) \in X \) unfolding FinPow_def
qed
Suppose we have a linear relation \(r\) on \(X\) and a subset \(B\subseteq X\) with an element \(x\in B\) such that there is only finite number of elements \(y\) of \(B\) for which \(\langle y,x\rangle\in r\). Then \(B\) has a minimum with the usual properties.
lemma leq_fin_has_min:
assumes \( \text{IsLinOrder}(X,r) \), \( B\subseteq X \), \( x\in B \) and \( \{y\in B.\ \langle y,x\rangle \in r\} \in \text{FinPow}(X) \)
shows \( \text{HasAminimum}(r,B) \), \( \text{Minimum}(r,B) \in B \), \( \forall y\in B.\ \langle \text{Minimum}(r,B),y\rangle \in r \)proof let \( A = \{y\in B.\ \langle y,x\rangle \in r\} \)
let \( k = \text{Minimum}(r,A) \)
from assms(1,2,3) have \( x\in X \), \( x\in A \) and \( \text{antisym}(r) \), \( \text{trans}(r) \), \( r \text{ is total on } X \) using total_is_refl unfolding IsLinOrder_def, refl_def
with assms(4) have \( \text{HasAminimum}(r,A) \) using fin_has_min
with \( \text{antisym}(r) \) have \( k\in B \), \( \langle k,x\rangle \in r \) and \( \forall y\in A.\ \langle k,y\rangle \in r \) using Order_ZF_4_L4
{
fix \( y \)
assume \( y\in B \)
from \( \forall y\in A.\ \langle k,y\rangle \in r \) have \( y\in A \longrightarrow \langle k,y\rangle \in r \)
moreover {
}
ultimately have \( \langle k,y\rangle \in r \)
assume \( y\notin A \)
with assms(2), \( y\in B \), \( r \text{ is total on } X \), \( x\in X \) have \( \langle x,y\rangle \in r \) unfolding IsTotal_def
with \( \text{trans}(r) \), \( \langle k,x\rangle \in r \) have \( \langle k,y\rangle \in r \) unfolding trans_def
hence \( \forall y\in B.\ \langle k,y\rangle \in r \)
with \( k\in B \) show \( \text{HasAminimum}(r,B) \) unfolding HasAminimum_def
with \( \text{antisym}(r) \) show \( \text{Minimum}(r,B) \in B \), \( \forall y\in B.\ \langle \text{Minimum}(r,B),y\rangle \in r \) using Order_ZF_4_L4
qed
Suppose we have a linear relation \(r\) on \(X\) and a subset \(B\subseteq X\) with an element \(x\in B\) such that there is only a finite number of elements \(y\) of \(B\) for which \(\langle x,y\rangle\in r\). Then \(B\) has a maximum with the usual properties.
lemma leq_fin_has_max:
assumes \( \text{IsLinOrder}(X,r) \), \( B\subseteq X \), \( x\in B \) and \( \{y\in B.\ \langle x,y\rangle \in r\} \in \text{FinPow}(X) \)
shows \( \text{HasAmaximum}(r,B) \), \( \text{Maximum}(r,B) \in B \), \( \forall y\in B.\ \langle y, \text{Maximum}(r,B)\rangle \in r \)proof let \( A = \{y\in B.\ \langle x,y\rangle \in r\} \)
let \( k = \text{Maximum}(r,A) \)
from assms(1,2,3) have \( x\in X \), \( x\in A \) and \( \text{antisym}(r) \), \( \text{trans}(r) \), \( r \text{ is total on } X \) using total_is_refl unfolding IsLinOrder_def, refl_def
with assms(4) have \( \text{HasAmaximum}(r,A) \) using fin_has_max
with \( \text{antisym}(r) \) have \( k\in B \), \( \langle x,k\rangle \in r \) and \( \forall y\in A.\ \langle y,k\rangle \in r \) using Order_ZF_4_L3
{
fix \( y \)
assume \( y\in B \)
from \( \forall y\in A.\ \langle y,k\rangle \in r \) have \( y\in A \longrightarrow \langle y,k\rangle \in r \)
moreover {
}
ultimately have \( \langle y,k\rangle \in r \)
assume \( y\notin A \)
with assms(2), \( y\in B \), \( r \text{ is total on } X \), \( x\in X \) have \( \langle y,x\rangle \in r \) unfolding IsTotal_def
with \( \text{trans}(r) \), \( \langle x,k\rangle \in r \) have \( \langle y,k\rangle \in r \) unfolding trans_def
hence \( \forall y\in B.\ \langle y,k\rangle \in r \)
with \( k\in B \) show \( \text{HasAmaximum}(r,B) \) unfolding HasAmaximum_def
with \( \text{antisym}(r) \) show \( \text{Maximum}(r,B) \in B \), \( \forall y\in B.\ \langle y, \text{Maximum}(r,B)\rangle \in r \) using Order_ZF_4_L3
qed
Every nonempty set of natural numbers has a minimum with the usual properties.
theorem subset_nat_has_min:
assumes \( B\subseteq nat \), \( B\neq \emptyset \)
shows \( \text{HasAminimum}(Le,B) \), \( \text{Minimum}(Le,B) \in B \), \( \forall n\in B.\ \text{Minimum}(Le,B) \leq n \)proof from assms(2) obtain \( n \) where \( n\in B \)
let \( A = \{k\in B.\ \langle k,n\rangle \in Le\} \)
from assms(1), \( n\in B \) have \( A \subseteq n + 1 \) using succ_add_one(1), nat_mem_lt(2) unfolding Le_def
then have \( A \in \text{FinPow}(nat) \) using nat_finpow_nat, subset_finpow
with assms(1), \( n\in B \) show \( \text{HasAminimum}(Le,B) \) and \( \text{Minimum}(Le,B) \in B \) using NatOrder_ZF_1_L2(4), leq_fin_has_min(1,2)
from assms(1), \( n\in B \), \( A \in \text{FinPow}(nat) \) have \( \forall y\in B.\ \langle \text{Minimum}(Le,B),y\rangle \in Le \) using NatOrder_ZF_1_L2(4), leq_fin_has_min(3)
then show \( \forall n\in B.\ \text{Minimum}(Le,B) \leq n \) unfolding Le_def
qed
Every nonempty subset of a natural number has a maximum with expected properties.
lemma nat_max_props:
assumes \( n\in nat \), \( A\subseteq n \), \( A\neq 0 \)
shows \( \text{Maximum}(Le,A) \in A \), \( \text{Maximum}(Le,A) \in nat \), \( \forall k\in A.\ k \leq \text{Maximum}(Le,A) \)proof from assms(1,2) have \( A \in \text{FinPow}(nat) \) using nat_finpow_nat, subset_finpow
with assms(3) show \( \text{Maximum}(Le,A) \in A \), \( \text{Maximum}(Le,A) \in nat \) using NatOrder_ZF_1_L2(4), linord_min_max_props(1,5)
from assms(3), \( A \in \text{FinPow}(nat) \) have \( \forall k\in A.\ \langle k, \text{Maximum}(Le,A)\rangle \in Le \) using linord_min_max_props(2), NatOrder_ZF_1_L2(4)
then show \( \forall k\in A.\ k \leq \text{Maximum}(Le,A) \)
qed
Yet another version of induction where the induction step is valid only up to \(n\in \mathbb{N}\) rather than for all natural numbers. This lemma is redundant as it is easier to prove this assertion using lemma fin_nat_ind from Nat_ZF_IML which was done in lemma fin_nat_ind1 there. It is left here for now as an alternative proof based on properties of the maximum of a finite set.
lemma ind_on_nat2:
assumes \( n\in nat \) and \( P(0) \) and \( \forall j\in n.\ P(j)\longrightarrow P(j + 1) \)
shows \( \forall j\in n + 1.\ P(j) \) and \( P(n) \)proof let \( A = \{k\in succ(n).\ \forall j\in succ(k).\ P(j)\} \)
let \( M = \text{Maximum}(Le,A) \)
from assms(1,2) have I: \( succ(n) \in nat \), \( A\subseteq succ(n) \), \( A\neq 0 \) using empty_in_every_succ
then have \( M \in A \) by (rule nat_max_props )
have \( n=M \)proof
from \( M \in A \) have \( M \in succ(n) \)
with assms(1) have \( M\in n \vee M=n \)
moreover {
}
ultimately show \( n=M \)
qed
assume \( M \in n \)
from I have \( M \in nat \) by (rule nat_max_props )
from assms(3), \( M\in A \), \( M\in n \) have \( P(M + 1) \)
with \( M \in nat \) have \( P(succ(M)) \) using succ_add_one(1)
with \( M\in A \) have \( \forall j\in succ(succ(M)).\ P(j) \)
moreover
from assms(1), \( M \in n \) have \( succ(M) \in succ(n) \) using succ_ineq1
moreover from I have \( \forall k\in A.\ k \leq M \) by (rule nat_max_props )
ultimately have \( False \)
with \( M \in A \) have \( n\in A \) by (rule eq_mem )
with assms(1) show \( \forall j\in n + 1.\ P(j) \) and \( P(n) \) using succ_add_one(1)
qed
Order isomorphisms of finite sets
In this section we establish that if two linearly ordered finite sets have the same number of elements, then they are order-isomorphic and the isomorphism is unique. This allows us to talk about ''enumeration'' of a linearly ordered finite set. We define the enumeration as the order isomorphism between the number of elements of the set (which is a natural number \(n = \{0,1,..,n-1\}\)) and the set.
A really weird corner case - empty set is order isomorphic with itself.
lemma empty_ord_iso:
shows \( ord\_iso(0,r,0,R) \neq 0 \)proof have \( 0 \approx 0 \) using eqpoll_refl
then obtain \( f \) where \( f \in \text{bij}(0,0) \) using eqpoll_def
then show \( thesis \) using ord_iso_def
qed
Even weirder than empty_ord_iso The order automorphism of the empty set is unique.
lemma empty_ord_iso_uniq:
assumes \( f \in ord\_iso(0,r,0,R) \), \( g \in ord\_iso(0,r,0,R) \)
shows \( f = g \)proof from assms have \( f : 0 \rightarrow 0 \) and \( g: 0 \rightarrow 0 \) using ord_iso_def, bij_def, surj_def
moreover
qed
have \( \forall x\in 0.\ f(x) = g(x) \)
ultimately show \( f = g \) by (rule func_eq )
The empty set is the only order automorphism of itself.
lemma empty_ord_iso_empty:
shows \( ord\_iso(0,r,0,R) = \{0\} \)proof have \( 0 \in ord\_iso(0,r,0,R) \)proof
have \( ord\_iso(0,r,0,R) \neq 0 \) by (rule empty_ord_iso )
then obtain \( f \) where \( f \in ord\_iso(0,r,0,R) \)
then show \( 0 \in ord\_iso(0,r,0,R) \) using ord_iso_def, bij_def, surj_def, fun_subset_prod
qed
then show \( ord\_iso(0,r,0,R) = \{0\} \) using empty_ord_iso_uniq
qed
An induction (or maybe recursion?) scheme for linearly ordered sets. The induction step is that we show that if the property holds when the set is a singleton or for a set with the maximum removed, then it holds for the set. The idea is that since we can build any finite set by adding elements on the right, then if the property holds for the empty set and is invariant with respect to this operation, then it must hold for all finite sets.
lemma fin_ord_induction:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( P(0) \) and A3: \( \forall A \in \text{FinPow}(X).\ A \neq 0 \longrightarrow (P(A - \{ \text{Maximum}(r,A)\}) \longrightarrow P(A)) \) and A4: \( B \in \text{FinPow}(X) \)
shows \( P(B) \)proof note A2
moreover
qed
have \( \forall A \in \text{FinPow}(X).\ A \neq 0 \longrightarrow (\exists a\in A.\ P(A-\{a\}) \longrightarrow P(A)) \)proof
moreover {
}
fix \( A \)
assume \( A \in \text{FinPow}(X) \) and \( A \neq 0 \)
with A1, A3 have \( \exists a\in A.\ P(A-\{a\}) \longrightarrow P(A) \) using IsLinOrder_def, fin_has_max, IsLinOrder_def, Order_ZF_4_L3
thus \( thesis \)
qed
note A4
ultimately show \( P(B) \) by (rule FinPow_ind_rem_one )
A sligltly more complicated version of fin_ord_induction that allows to prove properties that are not true for the empty set.
lemma fin_ord_ind:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( \forall A \in \text{FinPow}(X).\ \) \( A = 0 \vee (A = \{ \text{Maximum}(r,A)\} \vee P(A - \{ \text{Maximum}(r,A)\}) \longrightarrow P(A)) \) and A3: \( B \in \text{FinPow}(X) \) and A4: \( B\neq 0 \)
shows \( P(B) \)proof{
}
fix \( A \)
assume \( A \in \text{FinPow}(X) \) and \( A \neq 0 \)
with A1, A2 have \( \exists a\in A.\ A = \{a\} \vee P(A-\{a\}) \longrightarrow P(A) \) using IsLinOrder_def, fin_has_max, IsLinOrder_def, Order_ZF_4_L3
then have \( \forall A \in \text{FinPow}(X).\ \)
\( A = 0 \vee (\exists a\in A.\ A = \{a\} \vee P(A-\{a\}) \longrightarrow P(A)) \)
with A3, A4 show \( P(B) \) using FinPow_rem_ind
qed
Yet another induction scheme. We build a linearly ordered set by adding elements that are greater than all elements in the set.
lemma fin_ind_add_max:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( P(0) \) and A3: \( \forall A \in \text{FinPow}(X).\ \) \( ( \forall x \in X-A.\ P(A) \wedge (\forall a\in A.\ \langle a,x\rangle \in r ) \longrightarrow P(A \cup \{x\})) \) and A4: \( B \in \text{FinPow}(X) \)
shows \( P(B) \)proof note A1, A2
moreover
qed
have \( \forall C \in \text{FinPow}(X).\ C \neq 0 \longrightarrow (P(C - \{ \text{Maximum}(r,C)\}) \longrightarrow P(C)) \)proof
moreover {
}
fix \( C \)
assume \( C \in \text{FinPow}(X) \) and \( C \neq 0 \)
let \( x = \text{Maximum}(r,C) \)
let \( A = C - \{x\} \)
assume \( P(A) \)
moreover
from \( C \in \text{FinPow}(X) \) have \( A \in \text{FinPow}(X) \) using fin_rem_point_fin
moreover from A1, \( C \in \text{FinPow}(X) \), \( C \neq 0 \) have \( x \in C \) and \( x \in X - A \) and \( \forall a\in A.\ \langle a,x\rangle \in r \) using linord_min_max_props(1,2,5)
moreover note A3
ultimately have \( P(A \cup \{x\}) \)
moreover
from \( x \in C \) have \( A \cup \{x\} = C \)
ultimately have \( P(C) \)
thus \( thesis \)
qed
note A4
ultimately show \( P(B) \) by (rule fin_ord_induction )
The only order automorphism of a linearly ordered finite set is the identity.
theorem fin_ord_auto_id:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( B \in \text{FinPow}(X) \) and A3: \( B\neq 0 \)
shows \( ord\_iso(B,r,B,r) = \{id(B)\} \)proof note A1
moreover {
}
qed
fix \( A \)
assume \( A \in \text{FinPow}(X) \), \( A\neq 0 \)
let \( M = \text{Maximum}(r,A) \)
let \( A_0 = A - \{M\} \)
assume \( A = \{M\} \vee ord\_iso(A_0,r,A_0,r) = \{id(A_0)\} \)
moreover {
}
moreover {
}
ultimately have \( ord\_iso(A,r,A,r) = \{id(A)\} \)
assume \( A = \{M\} \)
have \( ord\_iso(\{M\},r,\{M\},r) = \{id(\{M\})\} \) using id_ord_auto_singleton
with \( A = \{M\} \) have \( ord\_iso(A,r,A,r) = \{id(A)\} \)
assume \( ord\_iso(A_0,r,A_0,r) = \{id(A_0)\} \)
have \( ord\_iso(A,r,A,r) = \{id(A)\} \)proof
}
show \( \{id(A)\} \subseteq ord\_iso(A,r,A,r) \) using id_ord_iso
{
fix \( f \)
assume \( f \in ord\_iso(A,r,A,r) \)
with A1, \( A \in \text{FinPow}(X) \), \( A\neq 0 \) have \( \text{restrict}(f,A_0) \in ord\_iso(A_0, r, A-\{f(M)\},r) \) using IsLinOrder_def, fin_has_max, ord_iso_rem_max
with A1, \( A \in \text{FinPow}(X) \), \( A\neq 0 \), \( f \in ord\_iso(A,r,A,r) \), \( ord\_iso(A_0,r,A_0,r) = \{id(A_0)\} \) have \( \text{restrict}(f,A_0) = id(A_0) \) using IsLinOrder_def, fin_has_max, max_auto_fixpoint
moreover
from A1, \( f \in ord\_iso(A,r,A,r) \), \( A \in \text{FinPow}(X) \), \( A\neq 0 \) have \( f : A \rightarrow A \) and \( M \in A \) and \( f(M) = M \) using ord_iso_def, bij_is_fun, IsLinOrder_def, fin_has_max, Order_ZF_4_L3, max_auto_fixpoint
ultimately have \( f = id(A) \) using id_fixpoint_rem
then show \( ord\_iso(A,r,A,r) \subseteq \{id(A)\} \)
qed
then have \( \forall A \in \text{FinPow}(X).\ A = 0 \vee \)
\( (A = \{ \text{Maximum}(r,A)\} \vee \)
\( ord\_iso(A-\{ \text{Maximum}(r,A)\},r,A-\{ \text{Maximum}(r,A)\},r) = \)
\( \{id(A-\{ \text{Maximum}(r,A)\})\} \longrightarrow ord\_iso(A,r,A,r) = \{id(A)\}) \)
moreover note A2, A3
ultimately show \( ord\_iso(B,r,B,r) = \{id(B)\} \) by (rule fin_ord_ind )
Every two finite linearly ordered sets are order isomorphic. The statement is formulated to make the proof by induction on the size of the set easier, see fin_ord_iso_ex for an alternative formulation.
lemma fin_order_iso:
assumes A1: \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and A2: \( n \in nat \)
shows \( \forall A \in \text{FinPow}(X).\ \forall B \in \text{FinPow}(Y).\ \) \( A \approx n \wedge B \approx n \longrightarrow ord\_iso(A,r,B,R) \neq 0 \)proof note A2
moreover
qed
have \( \forall A \in \text{FinPow}(X).\ \forall B \in \text{FinPow}(Y).\ \)
\( A \approx 0 \wedge B \approx 0 \longrightarrow ord\_iso(A,r,B,R) \neq 0 \) using eqpoll_0_is_0, empty_ord_iso
moreover have \( \forall k \in nat.\ \)
\( (\forall A \in \text{FinPow}(X).\ \forall B \in \text{FinPow}(Y).\ \)
\( A \approx k \wedge B \approx k \longrightarrow ord\_iso(A,r,B,R) \neq 0) \longrightarrow \)
\( (\forall C \in \text{FinPow}(X).\ \forall D \in \text{FinPow}(Y).\ \)
\( C \approx succ(k) \wedge D \approx succ(k) \longrightarrow ord\_iso(C,r,D,R) \neq 0) \)proof
ultimately show \( thesis \) by (rule ind_on_nat )
{
}
fix \( k \)
assume \( k \in nat \)
assume A3: \( \forall A \in \text{FinPow}(X).\ \forall B \in \text{FinPow}(Y).\ \)
\( A \approx k \wedge B \approx k \longrightarrow ord\_iso(A,r,B,R) \neq 0 \)
have \( \forall C \in \text{FinPow}(X).\ \forall D \in \text{FinPow}(Y).\ \)
\( C \approx succ(k) \wedge D \approx succ(k) \longrightarrow ord\_iso(C,r,D,R) \neq 0 \)proof
{
}
fix \( C \)
assume \( C \in \text{FinPow}(X) \)
fix \( D \)
assume \( D \in \text{FinPow}(Y) \)
assume \( C \approx succ(k) \), \( D \approx succ(k) \)
then have \( C \neq 0 \) and \( D\neq 0 \) using eqpoll_succ_imp_not_empty
let \( M_C = \text{Maximum}(r,C) \)
let \( M_D = \text{Maximum}(R,D) \)
let \( C_0 = C - \{M_C\} \)
let \( D_0 = D - \{M_D\} \)
from \( C \in \text{FinPow}(X) \) have \( C \subseteq X \) using FinPow_def
with A1 have \( \text{IsLinOrder}(C,r) \) using ord_linear_subset
from \( D \in \text{FinPow}(Y) \) have \( D \subseteq Y \) using FinPow_def
with A1 have \( \text{IsLinOrder}(D,R) \) using ord_linear_subset
from A1, \( C \in \text{FinPow}(X) \), \( D \in \text{FinPow}(Y) \), \( C \neq 0 \), \( D\neq 0 \) have \( \text{HasAmaximum}(r,C) \) and \( \text{HasAmaximum}(R,D) \) using IsLinOrder_def, fin_has_max
with A1 have \( M_C \in C \) and \( M_D \in D \) using IsLinOrder_def, Order_ZF_4_L3
with \( C \approx succ(k) \), \( D \approx succ(k) \) have \( C_0 \approx k \) and \( D_0 \approx k \) using Diff_sing_eqpoll
from \( C \in \text{FinPow}(X) \), \( D \in \text{FinPow}(Y) \) have \( C_0 \in \text{FinPow}(X) \) and \( D_0 \in \text{FinPow}(Y) \) using fin_rem_point_fin
with A3, \( C_0 \approx k \), \( D_0 \approx k \) have \( ord\_iso(C_0,r,D_0,R) \neq 0 \)
with \( \text{IsLinOrder}(C,r) \), \( \text{IsLinOrder}(D,R) \), \( \text{HasAmaximum}(r,C) \), \( \text{HasAmaximum}(R,D) \) have \( ord\_iso(C,r,D,R) \neq 0 \) by (rule rem_max_ord_iso )
thus \( thesis \)
qed
thus \( thesis \)
qed
Every two finite linearly ordered sets are order isomorphic.
lemma fin_ord_iso_ex:
assumes A1: \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and A2: \( A \in \text{FinPow}(X) \), \( B \in \text{FinPow}(Y) \) and A3: \( B \approx A \)
shows \( ord\_iso(A,r,B,R) \neq 0 \)proof from A2 obtain \( n \) where \( n \in nat \) and \( A \approx n \) using finpow_decomp
from A3, \( A \approx n \) have \( B \approx n \) by (rule eqpoll_trans )
with A1, A2, \( A \approx n \), \( n \in nat \) show \( ord\_iso(A,r,B,R) \neq 0 \) using fin_order_iso
qed
Existence and uniqueness of order isomorphism for two linearly ordered sets with the same number of elements.
theorem fin_ord_iso_ex_uniq:
assumes A1: \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and A2: \( A \in \text{FinPow}(X) \), \( B \in \text{FinPow}(Y) \) and A3: \( B \approx A \)
shows \( \exists !f.\ f \in ord\_iso(A,r,B,R) \)proof from assms show \( \exists f.\ f \in ord\_iso(A,r,B,R) \) using fin_ord_iso_ex
fix \( f \) \( g \)
assume A4: \( f \in ord\_iso(A,r,B,R) \), \( g \in ord\_iso(A,r,B,R) \)
then have \( converse(g) \in ord\_iso(B,R,A,r) \) using ord_iso_sym
with \( f \in ord\_iso(A,r,B,R) \) have I: \( converse(g)\circ f \in ord\_iso(A,r,A,r) \) by (rule ord_iso_trans )
{
assume \( A \neq 0 \)
with A1, A2, I have \( converse(g)\circ f = id(A) \) using fin_ord_auto_id
with A4 have \( f = g \) using ord_iso_def, comp_inv_id_eq_bij
moreover {
}
ultimately show \( f = g \) using ord_iso_def, comp_inv_id_eq_bij
qed
assume \( A = 0 \)
then have \( A \approx 0 \) using eqpoll_0_iff
with A3 have \( B \approx 0 \) by (rule eqpoll_trans )
with A4, \( A = 0 \) have \( f \in ord\_iso(0,r,0,R) \) and \( g \in ord\_iso(0,r,0,R) \) using eqpoll_0_iff
then have \( f = g \) by (rule empty_ord_iso_uniq )
end
lemma total_is_refl:
assumes \( r \text{ is total on } X \)
shows \( \text{refl}(X,r) \) lemma Order_ZF_4_L8:
assumes \( \text{refl}(X,r) \) and \( a\in X \)
shows \( \text{HasAmaximum}(r,\{a\}) \), \( \text{HasAminimum}(r,\{a\}) \)Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma Order_ZF_4_L9:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( A\subseteq X \) and \( a\in X \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAmaximum}(r,A\cup \{a\}) \) theorem FinPow_induct:
assumes \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ P(A) \longrightarrow (\forall a\in X.\ P(A \cup \{a\})) \) and \( B \in \text{FinPow}(X) \)
shows \( P(B) \) lemma Order_ZF_4_L8:
assumes \( \text{refl}(X,r) \) and \( a\in X \)
shows \( \text{HasAmaximum}(r,\{a\}) \), \( \text{HasAminimum}(r,\{a\}) \) lemma Order_ZF_4_L10:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( A\subseteq X \) and \( a\in X \) and \( \text{HasAminimum}(r,A) \)
shows \( \text{HasAminimum}(r,A\cup \{a\}) \) theorem fin_has_max:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( B \in \text{FinPow}(X) \) and \( B \neq 0 \)
shows \( \text{HasAmaximum}(r,B) \) theorem fin_has_min:
assumes \( r \text{ is total on } X \), \( \text{trans}(r) \), \( B \in \text{FinPow}(X) \), \( B\neq 0 \)
shows \( \text{HasAminimum}(r,B) \) lemma Order_ZF_4_L3:
assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \) lemma Order_ZF_4_L4:
assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \)
shows \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \)Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
Definition of IsTotal:
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of HasAminimum:
\( \text{HasAminimum}(r,A) \equiv \exists m\in A.\ \forall x\in A.\ \langle m,x\rangle \in r \)
Definition of HasAmaximum:
\( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) lemma nat_mem_lt:
assumes \( n\in nat \)
shows \( k \lt n \longleftrightarrow k\in n \) and \( k\leq n \longleftrightarrow k \in succ(n) \) lemma nat_finpow_nat:
assumes \( n \in nat \)
shows \( n \in \text{FinPow}(nat) \) lemma subset_finpow:
assumes \( A \in \text{FinPow}(X) \) and \( B \subseteq A \)
shows \( B \in \text{FinPow}(X) \) lemma NatOrder_ZF_1_L2: shows \( \text{antisym}(Le) \), \( \text{trans}(Le) \), \( Le \text{ is total on } nat \), \( \text{IsLinOrder}(nat,Le) \)
lemma leq_fin_has_min:
assumes \( \text{IsLinOrder}(X,r) \), \( B\subseteq X \), \( x\in B \) and \( \{y\in B.\ \langle y,x\rangle \in r\} \in \text{FinPow}(X) \)
shows \( \text{HasAminimum}(r,B) \), \( \text{Minimum}(r,B) \in B \), \( \forall y\in B.\ \langle \text{Minimum}(r,B),y\rangle \in r \) lemma leq_fin_has_min:
assumes \( \text{IsLinOrder}(X,r) \), \( B\subseteq X \), \( x\in B \) and \( \{y\in B.\ \langle y,x\rangle \in r\} \in \text{FinPow}(X) \)
shows \( \text{HasAminimum}(r,B) \), \( \text{Minimum}(r,B) \in B \), \( \forall y\in B.\ \langle \text{Minimum}(r,B),y\rangle \in r \) lemma linord_min_max_props:
assumes \( \text{IsLinOrder}(X,r) \), \( A \in \text{FinPow}(X) \), \( A\neq \emptyset \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall a\in A.\ \langle a, \text{Maximum}(r,A)\rangle \in r \), \( \text{Minimum}(r,A) \in A \), \( \forall a\in A.\ \langle \text{Minimum}(r,A),a\rangle \in r \), \( \text{Maximum}(r,A) \in X \), \( \text{Minimum}(r,A) \in X \) lemma linord_min_max_props:
assumes \( \text{IsLinOrder}(X,r) \), \( A \in \text{FinPow}(X) \), \( A\neq \emptyset \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall a\in A.\ \langle a, \text{Maximum}(r,A)\rangle \in r \), \( \text{Minimum}(r,A) \in A \), \( \forall a\in A.\ \langle \text{Minimum}(r,A),a\rangle \in r \), \( \text{Maximum}(r,A) \in X \), \( \text{Minimum}(r,A) \in X \) lemma empty_in_every_succ:
assumes \( n \in nat \)
shows \( 0 \in succ(n) \) lemma nat_max_props:
assumes \( n\in nat \), \( A\subseteq n \), \( A\neq 0 \)
shows \( \text{Maximum}(Le,A) \in A \), \( \text{Maximum}(Le,A) \in nat \), \( \forall k\in A.\ k \leq \text{Maximum}(Le,A) \) lemma succ_ineq1:
assumes \( n \in nat \), \( i\in n \)
shows \( succ(i) \in succ(n) \), \( i + 1 \in n + 1 \), \( i \in n + 1 \) lemma eq_mem:
assumes \( x\in A \) and \( y=x \)
shows \( y\in A \) lemma func_eq:
assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)
shows \( f = g \) lemma empty_ord_iso: shows \( ord\_iso(0,r,0,R) \neq 0 \)
lemma fun_subset_prod:
assumes \( f:X\rightarrow Y \)
shows \( f \subseteq X\times Y \) lemma empty_ord_iso_uniq:
assumes \( f \in ord\_iso(0,r,0,R) \), \( g \in ord\_iso(0,r,0,R) \)
shows \( f = g \) lemma FinPow_ind_rem_one:
assumes \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ A \neq 0 \longrightarrow (\exists a\in A.\ P(A-\{a\}) \longrightarrow P(A)) \) and \( B \in \text{FinPow}(X) \)
shows \( P(B) \) lemma FinPow_rem_ind:
assumes \( \forall A \in \text{FinPow}(X).\ \) \( A = 0 \vee (\exists a\in A.\ A = \{a\} \vee P(A-\{a\}) \longrightarrow P(A)) \) and \( A \in \text{FinPow}(X) \) and \( A\neq 0 \)
shows \( P(A) \) corollary fin_rem_point_fin:
assumes \( A \in \text{FinPow}(X) \)
shows \( A - \{a\} \in \text{FinPow}(X) \) lemma linord_min_max_props:
assumes \( \text{IsLinOrder}(X,r) \), \( A \in \text{FinPow}(X) \), \( A\neq \emptyset \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall a\in A.\ \langle a, \text{Maximum}(r,A)\rangle \in r \), \( \text{Minimum}(r,A) \in A \), \( \forall a\in A.\ \langle \text{Minimum}(r,A),a\rangle \in r \), \( \text{Maximum}(r,A) \in X \), \( \text{Minimum}(r,A) \in X \) lemma fin_ord_induction:
assumes \( \text{IsLinOrder}(X,r) \) and \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ A \neq 0 \longrightarrow (P(A - \{ \text{Maximum}(r,A)\}) \longrightarrow P(A)) \) and \( B \in \text{FinPow}(X) \)
shows \( P(B) \) lemma id_ord_auto_singleton: shows \( ord\_iso(\{x\},r,\{x\},r) = \{id(\{x\})\} \)
lemma id_ord_iso: shows \( id(X) \in ord\_iso(X,r,X,r) \)
corollary ord_iso_rem_max:
assumes \( \text{antisym}(r) \) and \( f \in ord\_iso(A,r,B,R) \) and \( \text{HasAmaximum}(r,A) \) and \( M = \text{Maximum}(r,A) \)
shows \( \text{restrict}(f,A-\{M\}) \in ord\_iso(A-\{M\}, r, B-\{f(M)\},R) \) lemma max_auto_fixpoint:
assumes \( \text{antisym}(r) \) and \( f \in ord\_iso(A,r,A,r) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{Maximum}(r,A) = f( \text{Maximum}(r,A)) \) lemma id_fixpoint_rem:
assumes \( f:X\rightarrow X \) and \( p\in X \) and \( f(p) = p \) and \( \text{restrict}(f, X-\{p\}) = id(X-\{p\}) \)
shows \( f = id(X) \) lemma fin_ord_ind:
assumes \( \text{IsLinOrder}(X,r) \) and \( \forall A \in \text{FinPow}(X).\ \) \( A = 0 \vee (A = \{ \text{Maximum}(r,A)\} \vee P(A - \{ \text{Maximum}(r,A)\}) \longrightarrow P(A)) \) and \( B \in \text{FinPow}(X) \) and \( B\neq 0 \)
shows \( P(B) \) lemma ord_linear_subset:
assumes \( \text{IsLinOrder}(X,r) \) and \( A\subseteq X \)
shows \( \text{IsLinOrder}(A,r) \) and \( \text{IsLinOrder}(A,r \cap A\times A) \) lemma rem_max_ord_iso:
assumes \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and \( \text{HasAmaximum}(r,X) \), \( \text{HasAmaximum}(R,Y) \), \( ord\_iso(X - \{ \text{Maximum}(r,X)\},r,Y - \{ \text{Maximum}(R,Y)\},R) \neq 0 \)
shows \( ord\_iso(X,r,Y,R) \neq 0 \) theorem ind_on_nat:
assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(succ(k)) \)
shows \( P(n) \) lemma finpow_decomp: shows \( \text{FinPow}(X) = (\bigcup n \in nat.\ \{A \in Pow(X).\ A \approx n\}) \)
lemma fin_order_iso:
assumes \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and \( n \in nat \)
shows \( \forall A \in \text{FinPow}(X).\ \forall B \in \text{FinPow}(Y).\ \) \( A \approx n \wedge B \approx n \longrightarrow ord\_iso(A,r,B,R) \neq 0 \) lemma fin_ord_iso_ex:
assumes \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and \( A \in \text{FinPow}(X) \), \( B \in \text{FinPow}(Y) \) and \( B \approx A \)
shows \( ord\_iso(A,r,B,R) \neq 0 \) theorem fin_ord_auto_id:
assumes \( \text{IsLinOrder}(X,r) \) and \( B \in \text{FinPow}(X) \) and \( B\neq 0 \)
shows \( ord\_iso(B,r,B,r) = \{id(B)\} \) lemma comp_inv_id_eq_bij:
assumes \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(A,B) \) and \( converse(b)\circ a = id(A) \)
shows \( a = b \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
