---

Step * of Lemma per-quotient-value-type

∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (value-type(a,b:A/per/E[a;b])) supposing (value-type(A) and EquivRel(A;a,b.E[a;b]))
BY
{ (ValueTypeAuto⋅ THEN (Assert a,b:A/per/E[a;b] ⋂ Base ⊆r A BY (RWO "per-quotient-isect-base" 0⋅ THEN Auto))) }

1
1. A : Type
2. E : A ⟶ A ⟶ ℙ
3. EquivRel(A;a,b.E[a;b])
4. value-type(A)
5. x : Base
6. x ∈ a,b:A/per/E[a;b]
7. v : a,b:A/per/E[a;b]
8. a,b:A/per/E[a;b] ⋂ Base ⊆r A
⊢ 0 ≤ eval v; 0

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (value-type(a,b:A/per/E[a;b]))  supposing  (value-type(A)  and  EquivRel(A;a,b.E[a;b]))


By

---

Latex:
(ValueTypeAuto\mcdot{}
  THEN  (Assert  a,b:A/per/E[a;b]  \mcap{}  Base  \msubseteq{}r  A  BY
                          (RWO  "per-quotient-isect-base"  0\mcdot{}  THEN  Auto))
  )

---

Home Index