---

Step * of Lemma perm_inverse

∀[T:Type]. ∀[p:Perm(T)].  ((p O inv_perm(p) = id_perm() ∈ Perm(T)) ∧ (inv_perm(p) O p = id_perm() ∈ Perm(T)))
BY
{ (GenUnivCD THENA Auto) }

1
1. T : Type
2. p : Perm(T)
⊢ p O inv_perm(p) = id_perm() ∈ Perm(T)

2
1. T : Type
2. p : Perm(T)
⊢ inv_perm(p) O p = id_perm() ∈ Perm(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:Perm(T)].    ((p  O  inv\_perm(p)  =  id\_perm())  \mwedge{}  (inv\_perm(p)  O  p  =  id\_perm()))


By

---

Latex:
(GenUnivCD  THENA  Auto)

---

Home Index