Step
*
1
1
of Lemma
geo-length-equality
1. e : BasicGeometry
2. p' : {p:Point| O_X_p}
3. v : Point
4. [%2] : O_X_v ∧ Xv ≅ Xp'
5. extend OX by Xp' = v ∈ {x:Point| O_X_x ∧ Xx ≅ Xp'}
⊢ v ≡ p'
BY
{ (InstLemma `geo-construction-unicity` [⌜e⌝;⌜O⌝;⌜X⌝;⌜p'⌝;⌜v⌝]⋅ THEN Auto) }
Latex:
Latex:
1. e : BasicGeometry
2. p' : \{p:Point| O\_X\_p\}
3. v : Point
4. [\%2] : O\_X\_v \mwedge{} Xv \00D0 Xp'
5. extend OX by Xp' = v
\mvdash{} v \mequiv{} p'
By
Latex:
(InstLemma `geo-construction-unicity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index