---

Step * 1 of Lemma finite-partition-property


1. k : ℕ
2. f : ℕ ⟶ ℕk
3. ∀i:ℕk. (¬(∀n:ℕ. (¬¬(∃m:ℕ. (n < m ∧ ((f m) = i ∈ ℤ))))))
⊢ False
BY
{ (Assert ∀i:ℕk. (¬¬(∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((f m) = i ∈ ℤ)))))) BY
         (RWO "not_over_exists" 0 THEN Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mforall{}i:\mBbbN{}k.  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((f  m)  =  i))))))  BY
              (RWO  "not\_over\_exists"  0  THEN  Auto))

---

Home Index