---

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


1. k : ℕ
2. f : ℕ ⟶ ℕk
3. ∀i:ℕk. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((f m) = i ∈ ℤ))))
⊢ ∃n:ℕ. ∀i:ℕk. (¬(∃m:ℕ. (n < m ∧ ((f m) = i ∈ ℤ))))
BY
{ (MoveToConcl (-1) THEN (GenConcl ⌜f = g ∈ (ℕ ⟶ ℤ)⌝⋅ THENA Auto) THEN ThinVar `f') }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `f')

---

Home Index