---

Step * 1 1 1 of Lemma decidable__quotient_equal


1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. f : T ⟶ T ⟶ 𝔹
5. ∀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]))
BY
{ Assert ⌜f ∈ (x,y:T//E[x;y]) ⟶ (x,y:T//E[x;y]) ⟶ 𝔹⌝ }

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

2
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. f : T ⟶ T ⟶ 𝔹
5. ∀x,y:T.  (↑(x f y) ⇐⇒ E[x;y])
6. f ∈ (x,y:T//E[x;y]) ⟶ (x,y:T//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.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}x,y:T.    (\muparrow{}(x  f  y)  \mLeftarrow{}{}\mRightarrow{}  E[x;y])
\mvdash{}  \mexists{}f:(x,y:T//E[x;y])  {}\mrightarrow{}  (x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbB{}.  \mforall{}u,v:x,y:T//E[x;y].    (\muparrow{}(u  f  v)  \mLeftarrow{}{}\mRightarrow{}  u  =  v)


By

---

Latex:
Assert  \mkleeneopen{}f  \mmember{}  (x,y:T//E[x;y])  {}\mrightarrow{}  (x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}

---

Home Index