---

Step * of Lemma preima_of_equiv_rel

∀A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.  (EquivRel(B;x,y.x R y) ⇒ EquivRel(A;x,y.x R_f y))
BY
{ (Unfolds ``equiv_rel preima_of_rel`` 0 THEN Unfolds ``refl sym trans`` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.    (EquivRel(B;x,y.x  R  y)  {}\mRightarrow{}  EquivRel(A;x,y.x  R\_f  y))


By

---

Latex:
(Unfolds  ``equiv\_rel  preima\_of\_rel``  0  THEN  Unfolds  ``refl  sym  trans``  0  THEN  Reduce  0  THEN  Auto)

---

Home Index