theory Finite_ZF_1 imports Finite1 Order_ZF_1a
begin
This theory is based on Finite1 theory and is obsolete. It contains properties of finite sets related to order relations. See the FinOrd theory for a better approach.
Finite vs. bounded sets
The goal of this section is to show that finite sets are bounded and have maxima and minima.
Finite set has a maximum - induction step.
lemma Finite_ZF_1_1_L1:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( A\in Fin(X) \) and A4: \( x\in X \) and A5: \( A=0 \vee \text{HasAmaximum}(r,A) \)
shows \( A\cup \{x\} = 0 \vee \text{HasAmaximum}(r,A\cup \{x\}) \)proof{
}
assume \( A=0 \)
then have T1: \( A\cup \{x\} = \{x\} \)
from A1 have \( \text{refl}(X,r) \) using total_is_refl
with T1, A4 have \( A\cup \{x\} = 0 \vee \text{HasAmaximum}(r,A\cup \{x\}) \) using Order_ZF_4_L8
moreover {
}
ultimately show \( thesis \)
qed
assume \( A\neq 0 \)
with A1, A2, A3, A4, A5 have \( A\cup \{x\} = 0 \vee \text{HasAmaximum}(r,A\cup \{x\}) \) using FinD, Order_ZF_4_L9
For total and transitive relations finite set has a maximum.
theorem Finite_ZF_1_1_T1A:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( B\in Fin(X) \)
shows \( B=0 \vee \text{HasAmaximum}(r,B) \)proof have \( 0=0 \vee \text{HasAmaximum}(r,0) \)
moreover
qed
note A3
moreover from A1, A2 have \( \forall A\in Fin(X).\ \forall x\in X.\ \)
\( x\notin A \wedge (A=0 \vee \text{HasAmaximum}(r,A)) \longrightarrow (A\cup \{x\}=0 \vee \text{HasAmaximum}(r,A\cup \{x\})) \) using Finite_ZF_1_1_L1
ultimately show \( B=0 \vee \text{HasAmaximum}(r,B) \) by (rule Finite1_L16B )
Finite set has a minimum - induction step.
lemma Finite_ZF_1_1_L2:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( A\in Fin(X) \) and A4: \( x\in X \) and A5: \( A=0 \vee \text{HasAminimum}(r,A) \)
shows \( A\cup \{x\} = 0 \vee \text{HasAminimum}(r,A\cup \{x\}) \)proof{
}
assume \( A=0 \)
then have T1: \( A\cup \{x\} = \{x\} \)
from A1 have \( \text{refl}(X,r) \) using total_is_refl
with T1, A4 have \( A\cup \{x\} = 0 \vee \text{HasAminimum}(r,A\cup \{x\}) \) using Order_ZF_4_L8
moreover {
}
ultimately show \( thesis \)
qed
assume \( A\neq 0 \)
with A1, A2, A3, A4, A5 have \( A\cup \{x\} = 0 \vee \text{HasAminimum}(r,A\cup \{x\}) \) using FinD, Order_ZF_4_L10
For total and transitive relations finite set has a minimum.
theorem Finite_ZF_1_1_T1B:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( B \in Fin(X) \)
shows \( B=0 \vee \text{HasAminimum}(r,B) \)proof have \( 0=0 \vee \text{HasAminimum}(r,0) \)
moreover
qed
note A3
moreover from A1, A2 have \( \forall A\in Fin(X).\ \forall x\in X.\ \)
\( x\notin A \wedge (A=0 \vee \text{HasAminimum}(r,A)) \longrightarrow (A\cup \{x\}=0 \vee \text{HasAminimum}(r,A\cup \{x\})) \) using Finite_ZF_1_1_L2
ultimately show \( B=0 \vee \text{HasAminimum}(r,B) \) by (rule Finite1_L16B )
For transitive and total relations finite sets are bounded.
theorem Finite_ZF_1_T1:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( B\in Fin(X) \)
shows \( \text{IsBounded}(B,r) \)proof from A1, A2, A3 have \( B=0 \vee \text{HasAminimum}(r,B) \), \( B=0 \vee \text{HasAmaximum}(r,B) \) using Finite_ZF_1_1_T1A, Finite_ZF_1_1_T1B
then have \( B = 0 \vee \text{IsBoundedBelow}(B,r) \), \( B = 0 \vee \text{IsBoundedAbove}(B,r) \) using Order_ZF_4_L7, Order_ZF_4_L8A
then show \( \text{IsBounded}(B,r) \) using IsBounded_def, IsBoundedBelow_def, IsBoundedAbove_def
qed
For linearly ordered finite sets maximum and minimum have desired properties. The reason we need linear order is that we need the order to be total and transitive for the finite sets to have a maximum and minimum and then we also need antisymmetry for the maximum and minimum to be unique.
theorem Finite_ZF_1_T2:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( A \in Fin(X) \) and A3: \( A\neq 0 \)
shows \( \text{Maximum}(r,A) \in A \), \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \)proof from A1 have T1: \( r \text{ is total on } X \), \( \text{trans}(r) \), \( \text{antisym}(r) \) using IsLinOrder_def
moreover
qed
from T1, A2, A3 have \( \text{HasAmaximum}(r,A) \) using Finite_ZF_1_1_T1A
moreover from T1, A2, A3 have \( \text{HasAminimum}(r,A) \) using Finite_ZF_1_1_T1B
ultimately show \( \text{Maximum}(r,A) \in A \), \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \) using Order_ZF_4_L3, Order_ZF_4_L4
A special case of Finite_ZF_1_T2 when the set has three elements.
corollary Finite_ZF_1_L2A:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( a\in X \), \( b\in X \), \( c\in X \)
shows \( \text{Maximum}(r,\{a,b,c\}) \in \{a,b,c\} \), \( \text{Minimum}(r,\{a,b,c\}) \in \{a,b,c\} \), \( \text{Maximum}(r,\{a,b,c\}) \in X \), \( \text{Minimum}(r,\{a,b,c\}) \in X \), \( \langle a, \text{Maximum}(r,\{a,b,c\})\rangle \in r \), \( \langle b, \text{Maximum}(r,\{a,b,c\})\rangle \in r \), \( \langle c, \text{Maximum}(r,\{a,b,c\})\rangle \in r \)proof from A2 have I: \( \{a,b,c\} \in Fin(X) \), \( \{a,b,c\} \neq 0 \)
with A1 show II: \( \text{Maximum}(r,\{a,b,c\}) \in \{a,b,c\} \) by (rule Finite_ZF_1_T2 )
moreover
from A1, I show III: \( \text{Minimum}(r,\{a,b,c\}) \in \{a,b,c\} \) by (rule Finite_ZF_1_T2 )
moreover from A2 have \( \{a,b,c\} \subseteq X \)
ultimately show \( \text{Maximum}(r,\{a,b,c\}) \in X \), \( \text{Minimum}(r,\{a,b,c\}) \in X \)
from A1, I have \( \forall x\in \{a,b,c\}.\ \langle x, \text{Maximum}(r,\{a,b,c\})\rangle \in r \) by (rule Finite_ZF_1_T2 )
then show \( \langle a, \text{Maximum}(r,\{a,b,c\})\rangle \in r \), \( \langle b, \text{Maximum}(r,\{a,b,c\})\rangle \in r \), \( \langle c, \text{Maximum}(r,\{a,b,c\})\rangle \in r \)
qed
If for every element of \(X\) we can find one in \(A\) that is greater, then the \(A\) can not be finite. Works for relations that are total, transitive and antisymmetric.
lemma Finite_ZF_1_1_L3:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( \text{antisym}(r) \) and A4: \( r \subseteq X\times X \) and A5: \( X\neq 0 \) and A6: \( \forall x\in X.\ \exists a\in A.\ x\neq a \wedge \langle x,a\rangle \in r \)
shows \( A \notin Fin(X) \)proof from assms have \( \neg \text{IsBounded}(A,r) \) using Order_ZF_3_L14, IsBounded_def
with A1, A2 show \( A \notin Fin(X) \) using Finite_ZF_1_T1
qed
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\}) \) 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\}) \) lemma Finite_ZF_1_1_L1:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( A\in Fin(X) \) and \( x\in X \) and \( A=0 \vee \text{HasAmaximum}(r,A) \)
shows \( A\cup \{x\} = 0 \vee \text{HasAmaximum}(r,A\cup \{x\}) \) lemma Finite1_L16B:
assumes \( P(0) \) and \( B\in Fin(X) \) and \( \forall A\in Fin(X).\ \forall x\in X.\ x\notin A \wedge P(A)\longrightarrow P(A\cup \{x\}) \)
shows \( P(B) \) 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\}) \) lemma Finite_ZF_1_1_L2:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( A\in Fin(X) \) and \( x\in X \) and \( A=0 \vee \text{HasAminimum}(r,A) \)
shows \( A\cup \{x\} = 0 \vee \text{HasAminimum}(r,A\cup \{x\}) \) theorem Finite_ZF_1_1_T1A:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( B\in Fin(X) \)
shows \( B=0 \vee \text{HasAmaximum}(r,B) \) theorem Finite_ZF_1_1_T1B:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( B \in Fin(X) \)
shows \( B=0 \vee \text{HasAminimum}(r,B) \) lemma Order_ZF_4_L7:
assumes \( \text{HasAmaximum}(r,A) \)
shows \( \text{IsBoundedAbove}(A,r) \) lemma Order_ZF_4_L8A:
assumes \( \text{HasAminimum}(r,A) \)
shows \( \text{IsBoundedBelow}(A,r) \)Definition of IsBounded:
\( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
Definition of IsBoundedBelow:
\( \text{IsBoundedBelow}(A,r) \equiv (A=0 \vee (\exists l.\ \forall x\in A.\ \langle l,x\rangle \in r)) \)
Definition of IsBoundedAbove:
\( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\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) \)
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 \) theorem Finite_ZF_1_T2:
assumes \( \text{IsLinOrder}(X,r) \) and \( A \in Fin(X) \) and \( A\neq 0 \)
shows \( \text{Maximum}(r,A) \in A \), \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \) lemma Order_ZF_3_L14:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{antisym}(r) \) and \( r \subseteq X\times X \) and \( X\neq 0 \) and \( \forall x\in X.\ \exists a\in A.\ x\neq a \wedge \langle x,a\rangle \in r \)
shows \( \neg \text{IsBoundedAbove}(A,r) \) theorem Finite_ZF_1_T1:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( B\in Fin(X) \)
shows \( \text{IsBounded}(B,r) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8