---

Step * of Lemma pigeon-hole

∀[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm].  n ≤ m supposing Inj(ℕn;ℕm;f)
BY
{ (((Auto THEN InstLemma `finite-partition` [⌜n⌝;⌜m⌝;⌜f⌝]) THENA Auto) THEN ExRepD) }

1
1. n : ℕ
2. m : ℕ
3. f : ℕn ⟶ ℕm
4. Inj(ℕn;ℕm;f)
5. p : ℕm ⟶ (ℕ List)
6. Σ(||p j|| | j < m) = n ∈ ℤ
7. ∀j:ℕm. ∀x,y:ℕ||p j||.  p j[x] > p j[y] supposing x < y
8. ∀j:ℕm. ∀x:ℕ||p j||.  (p j[x] < n c∧ ((f p j[x]) = j ∈ ℤ))
⊢ n ≤ m

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m].    n  \mleq{}  m  supposing  Inj(\mBbbN{}n;\mBbbN{}m;f)


By

---

Latex:
(((Auto  THEN  InstLemma  `finite-partition`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}])  THENA  Auto)  THEN  ExRepD)

---

Home Index