---

Step * of Lemma pgeo-primitives_wf

No Annotations
ProjGeomPrimitives ∈ 𝕌'
BY
{ (Unfold `pgeo-primitives` 0 THEN Unfold `pgeo-line` 0) }

1
"Point":Type
"Line":Type
"PS":Point ⟶ self."Line" ⟶ ℙ ∈ 𝕌'

---

Latex:

---

Latex:
No  Annotations
ProjGeomPrimitives  \mmember{}  \mBbbU{}'


By

---

Latex:
(Unfold  `pgeo-primitives`  0  THEN  Unfold  `pgeo-line`  0)

---

Home Index