---

Step * of Lemma finite-partition-property

∀k:ℕ. ∀f:ℕ ⟶ ℕk.  (¬¬(∃i:ℕk. ∀n:ℕ. (¬¬(∃m:ℕ. (n < m ∧ ((f m) = i ∈ ℤ))))))
BY
{ (Auto THEN (RWO "not_over_exists" 0 THENA Auto) THEN (D 0 THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (RWO  "not\_over\_exists"  0  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index