---

Step * of Lemma pigeon-hole-implies2

∀n:ℕ
  ∀[m:ℕ]
    ∀f:ℕn ⟶ ℕm. ∀g:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕn [((f i) = (g j) ∈ ℤ)]) supposing Inj(ℕn;ℕm;g) supposing Inj(ℕn;ℕm;f) 
    supposing m < 2 * n
BY
{ (Auto
   THEN (InstLemma `pigeon-hole-implies-ext` [⌜2 * n⌝;⌜m⌝;⌜λi.if (i) < (n)  then f i  else (g (i - n))⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN ExRepD) }

1
1. n : ℕ@i
2. [m] : ℕ
3. m < 2 * n
4. f : ℕn ⟶ ℕm@i
5. Inj(ℕn;ℕm;f)
6. g : ℕn ⟶ ℕm@i
7. Inj(ℕn;ℕm;g)
8. i : ℕ2 * n
9. j : ℕi
10. if (i) < (n)  then f i  else (g (i - n)) = if (j) < (n)  then f j  else (g (j - n)) ∈ ℤ
⊢ ∃i:ℕn. (∃j:ℕn [((f i) = (g j) ∈ ℤ)])

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[m:\mBbbN{}]
        \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m
            \mforall{}g:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m.  \mexists{}i:\mBbbN{}n.  (\mexists{}j:\mBbbN{}n  [((f  i)  =  (g  j))])  supposing  Inj(\mBbbN{}n;\mBbbN{}m;g)  supposing  Inj(\mBbbN{}n;\mBbbN{}m;f) 
        supposing  m  <  2  *  n


By

---

Latex:
(Auto
  THEN  (InstLemma  `pigeon-hole-implies-ext`  [\mkleeneopen{}2  *  n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};
              \mkleeneopen{}\mlambda{}i.if  (i)  <  (n)    then  f  i    else  (g  (i  -  n))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  ExRepD)

---

Home Index