---

Step * of Lemma inv_image_ind

∀[A:Type]. ∀[r:A ⟶ A ⟶ ℙ]. ∀[B:Type].  ∀f:B ⟶ A. (WellFnd{i}(A;x,y.r[x;y]) ⇒ WellFnd{i}(B;x,y.r[f x;f y]))
BY
{ Lemma `inv_image_ind_tp` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[r:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:Type].
    \mforall{}f:B  {}\mrightarrow{}  A.  (WellFnd\{i\}(A;x,y.r[x;y])  {}\mRightarrow{}  WellFnd\{i\}(B;x,y.r[f  x;f  y]))


By

---

Latex:
Lemma  `inv\_image\_ind\_tp`

---

Home Index