---

Step * 1 1 1 1 1 1 1 1 of Lemma finite-partition-property


1. k : ℕ
2. g : ℕ ⟶ ℤ
⊢ (∀i:ℕk. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))) ⇒ (∃n:ℕ. ∀i:ℕk. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ)))))
BY
{ (NatInd 1 THEN Auto) }

1
1. g : ℕ ⟶ ℤ
2. ∀i:ℕ0. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))
⊢ ∃n:ℕ. ∀i:ℕ0. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))

2
1. g : ℕ ⟶ ℤ
2. k : ℤ
3. [%1] : 0 < k
4. (∀i:ℕk - 1. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))) ⇒ (∃n:ℕ. ∀i:ℕk - 1. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ)))))
5. ∀i:ℕk. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))
⊢ ∃n:ℕ. ∀i:ℕk. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  (\mforall{}i:\mBbbN{}k.  \mexists{}n:\mBbbN{}.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((g  m)  =  i)))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}k.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((g  m)  =  i)))))


By

---

Latex:
(NatInd  1  THEN  Auto)

---

Home Index