---

Step * of Lemma quotient-mono

∀[T:Type]. (mono(T) ⇒ (∀E:T ⟶ T ⟶ ℙ. (EquivRel(T;x,y.E[x;y]) ⇒ mono(x,y:T//E[x;y]))))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. T : Type
2. mono(T)
3. E : T ⟶ T ⟶ ℙ
4. EquivRel(T;x,y.E[x;y])
5. a : x,y:T//E[x;y]
6. b : Base
7. is-above(x,y:T//E[x;y];a;b)
⊢ a = b ∈ (x,y:T//E[x;y])

---

Latex:

---

Latex:
\mforall{}[T:Type].  (mono(T)  {}\mRightarrow{}  (\mforall{}E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (EquivRel(T;x,y.E[x;y])  {}\mRightarrow{}  mono(x,y:T//E[x;y]))))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index