---

Step * of Lemma p-fun-exp-injection

∀[A:Type]. ∀[f:A ⟶ (A + Top)].  ∀[n:ℕ]. p-inject(A;A;f^n) supposing p-inject(A;A;f)
BY
{ xxx(InductionOnNat THEN Auto)xxx }

1
.....basecase..... 
1. A : Type
2. f : A ⟶ (A + Top)
3. p-inject(A;A;f)
4. n : ℤ
⊢ p-inject(A;A;f^0)

2
.....upcase..... 
1. A : Type
2. f : A ⟶ (A + Top)
3. p-inject(A;A;f)
4. n : ℤ
5. 0 < n
6. p-inject(A;A;f^n - 1)
⊢ p-inject(A;A;f^n)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].    \mforall{}[n:\mBbbN{}].  p-inject(A;A;f\^{}n)  supposing  p-inject(A;A;f)


By

---

Latex:
xxx(InductionOnNat  THEN  Auto)xxx

---

Home Index