---

Step * of Lemma increasing_inj

∀[k,m:ℕ]. ∀[f:ℕk ⟶ ℕm].  Inj(ℕk;ℕm;f) supposing increasing(f;k)
BY
{ (Unfold `inject` 0 THEN Auto) }

1
1. k : ℕ
2. m : ℕ
3. f : ℕk ⟶ ℕm
4. increasing(f;k)
5. a1 : ℕk
6. a2 : ℕk
7. (f a1) = (f a2) ∈ ℕm
⊢ a1 = a2 ∈ ℕk

---

Latex:

---

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


By

---

Latex:
(Unfold  `inject`  0  THEN  Auto)

---

Home Index