---

Step * of Lemma not-inject

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀n:ℕ. ∀f:ℕn ⟶ T.  ∃i:ℕn. ∃j:ℕi. ((f i) = (f j) ∈ T) supposing ¬Inj(ℕn;T;f)))
BY
{ (Auto THEN Unfold `inject` (-1) THEN RepeatFor 2 (((RWO "not-all-int_seg" (-1) THENA Auto) THEN D -1))) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. n : ℕ@i
4. f : ℕn ⟶ T@i
5. a1 : ℕn
6. a2 : ℕn
7. ¬(((f a1) = (f a2) ∈ T) ⇒ (a1 = a2 ∈ ℕn))
⊢ ∃i:ℕn. ∃j:ℕi. ((f i) = (f j) ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  T.    \mexists{}i:\mBbbN{}n.  \mexists{}j:\mBbbN{}i.  ((f  i)  =  (f  j))  supposing  \mneg{}Inj(\mBbbN{}n;T;f)))


By

---

Latex:
(Auto
  THEN  Unfold  `inject`  (-1)
  THEN  RepeatFor  2  (((RWO  "not-all-int\_seg"  (-1)  THENA  Auto)  THEN  D  -1)))

---

Home Index