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 (((RWO "not-all-int_seg" (-1) THENA Auto) THEN -1))) }

1
1. [T] Type
2. ∀x,y:T.  Dec(x y ∈ T)@i
3. : ℕ@i
4. : ℕ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