---

Step * of Lemma equiv_rel-wf-per-quotient

∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].
  (EquivRel(T;x,y.↑E2[x;y])
  ⇒ EquivRel(T;x,y.↑E1[x;y])
  ⇒ (∀x,y:T.  ((↑E2[x;y]) ⇒ (↑E1[x;y])))
  ⇒ (E1 ∈ (x,y:T/per/(↑E2[x;y])) ⟶ (x,y:T/per/(↑E2[x;y])) ⟶ 𝔹))
BY
{ (TACTIC:InstLemma `equiv_rel-wf-quotient` [] THEN NthHypSq (-1) THEN Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E1,E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
    (EquivRel(T;x,y.\muparrow{}E2[x;y])
    {}\mRightarrow{}  EquivRel(T;x,y.\muparrow{}E1[x;y])
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((\muparrow{}E2[x;y])  {}\mRightarrow{}  (\muparrow{}E1[x;y])))
    {}\mRightarrow{}  (E1  \mmember{}  (x,y:T/per/(\muparrow{}E2[x;y]))  {}\mrightarrow{}  (x,y:T/per/(\muparrow{}E2[x;y]))  {}\mrightarrow{}  \mBbbB{}))


By

---

Latex:
(TACTIC:InstLemma  `equiv\_rel-wf-quotient`  []  THEN  NthHypSq  (-1)  THEN  Auto  THEN  Computation)

---

Home Index