---

Step * 1 1 1 1 of Lemma injections-combinations


1. n : ℕ
2. T : Type
3. f : ℕn ⟶ T
4. Inj(ℕn;T;f)
5. i : ℕ
6. j : ℕ
7. i < n
8. j < n
9. ¬(i = j ∈ ℕ)
⊢ ¬((f i) = (f j) ∈ T)
BY
{ TACTIC:ParallelLast }

1
1. n : ℕ
2. T : Type
3. f : ℕn ⟶ T
4. Inj(ℕn;T;f)
5. i : ℕ
6. j : ℕ
7. i < n
8. j < n
9. (f i) = (f j) ∈ T
⊢ i = j ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  T  :  Type
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  Inj(\mBbbN{}n;T;f)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  n
8.  j  <  n
9.  \mneg{}(i  =  j)
\mvdash{}  \mneg{}((f  i)  =  (f  j))


By

---

Latex:
TACTIC:ParallelLast

---

Home Index