---

Step * 1 of Lemma decidable__quotient_equal


1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. ∀x,y:T.  Dec(E[x;y])
⊢ ∀u,v:x,y:T//E[x;y].  Dec(u = v ∈ (x,y:T//E[x;y]))
BY
{ ((RWO "dec_iff_ex_bvfun" 0⋅ THENA Auto) THEN (RWO "dec_iff_ex_bvfun" 4⋅ THENA Auto)) }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. ∃f:T ⟶ T ⟶ 𝔹. ∀x,y:T.  (↑(x f y) ⇐⇒ E[x;y])
⊢ ∃f:(x,y:T//E[x;y]) ⟶ (x,y:T//E[x;y]) ⟶ 𝔹. ∀u,v:x,y:T//E[x;y].  (↑(u f v) ⇐⇒ u = v ∈ (x,y:T//E[x;y]))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [E]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.E[x;y])
4.  \mforall{}x,y:T.    Dec(E[x;y])
\mvdash{}  \mforall{}u,v:x,y:T//E[x;y].    Dec(u  =  v)


By

---

Latex:
((RWO  "dec\_iff\_ex\_bvfun"  0\mcdot{}  THENA  Auto)  THEN  (RWO  "dec\_iff\_ex\_bvfun"  4\mcdot{}  THENA  Auto))

---

Home Index