---

Step * of Lemma funinv_wf3

∀[n:ℕ]. ∀[f:ℕn →⟶ ℕn].  (inv(f) ∈ ℕn →⟶ ℕn)
BY
{ ((InstLemma `funinv_wf2` [] THEN Fold `injection` (-1)) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n].    (inv(f)  \mmember{}  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n)


By

---

Latex:
((InstLemma  `funinv\_wf2`  []  THEN  Fold  `injection`  (-1))  THEN  Trivial)

---

Home Index