---

Step * of Lemma perm_morph_wf

∀S,T:Type. ∀s2t:S ⟶ T. ∀t2s:T ⟶ S.  (InvFuns(S;T;s2t;t2s) ⇒ (∀p:Perm(S). (perm_morph(S;T;s2t;t2s;p) ∈ Perm(T))))
BY
{ ProveWfLemma }

1
1. S : Type
2. T : Type
3. s2t : S ⟶ T
4. t2s : T ⟶ S
5. InvFuns(S;T;s2t;t2s)
6. p : Perm(S)
⊢ InvFuns(T;T;s2t o (p.f o t2s);s2t o (p.b o t2s))

---

Latex:

---

Latex:
\mforall{}S,T:Type.  \mforall{}s2t:S  {}\mrightarrow{}  T.  \mforall{}t2s:T  {}\mrightarrow{}  S.
    (InvFuns(S;T;s2t;t2s)  {}\mRightarrow{}  (\mforall{}p:Perm(S).  (perm\_morph(S;T;s2t;t2s;p)  \mmember{}  Perm(T))))


By

---

Latex:
ProveWfLemma

---

Home Index