---

Step * 1 1 1 of Lemma injective-quotient-inject

.....aux..... 
1. T : Type
2. S : Type
3. f : T ⟶ S
4. {f ∈ T//x.f[x] ⟶ S}
5. a1 : Base
6. a3 : Base
7. a1 = a3 ∈ (x,y:T//((f x) = (f y) ∈ S))
8. a1 ∈ T
9. a3 ∈ T
10. (f a1) = (f a3) ∈ S
11. a2 : Base
12. a4 : Base
13. a2 = a4 ∈ (x,y:T//((f x) = (f y) ∈ S))
14. a2 ∈ T
15. a4 ∈ T
16. (f a2) = (f a4) ∈ S
17. (f a1) = (f a2) ∈ S
⊢ EquivRel(T;x,y.(f x) = (f y) ∈ S)
BY
{ (RepeatFor 2 (D 0) THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  T  :  Type
2.  S  :  Type
3.  f  :  T  {}\mrightarrow{}  S
4.  \{f  \mmember{}  T//x.f[x]  {}\mrightarrow{}  S\}
5.  a1  :  Base
6.  a3  :  Base
7.  a1  =  a3
8.  a1  \mmember{}  T
9.  a3  \mmember{}  T
10.  (f  a1)  =  (f  a3)
11.  a2  :  Base
12.  a4  :  Base
13.  a2  =  a4
14.  a2  \mmember{}  T
15.  a4  \mmember{}  T
16.  (f  a2)  =  (f  a4)
17.  (f  a1)  =  (f  a2)
\mvdash{}  EquivRel(T;x,y.(f  x)  =  (f  y))


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index