Step * of Lemma increasing_inj

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

1
1. : ℕ
2. : ℕ
3. : ℕ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