---

Step * of Lemma rel_inverse_exp

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀n:ℕ. ∀x,y:T.  (x R^n^-1 y ⇐⇒ x R^-1^n y)
BY
{ InductionOnNat }

1
.....basecase..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
⊢ ∀x,y:T.  (x R^0^-1 y ⇐⇒ x R^-1^0 y)

2
.....upcase..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. n : ℤ
4. [%1] : 0 < n
5. ∀x,y:T.  (x R^n - 1^-1 y ⇐⇒ x R^-1^n - 1 y)
⊢ ∀x,y:T.  (x R^n^-1 y ⇐⇒ x R^-1^n y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}n:\mBbbN{}.  \mforall{}x,y:T.    (x  rel\_exp(T;  R;  n)\^{}-1  y  \mLeftarrow{}{}\mRightarrow{}  x  rel\_exp(T;  R\^{}-1;  n)  y)


By

---

Latex:
InductionOnNat

---

Home Index