Nuprl Lemma : P_point-line-sep_wf
∀[eu:EuclideanParPlane]. ∀P:P_point(eu). ∀n:P_line(eu). (P_point-line-sep(eu;P;n) ∈ ℙ)
Proof
Error : references
Latex:
\mforall{}[eu:EuclideanParPlane]. \mforall{}P:P\_point(eu). \mforall{}n:P\_line(eu). (P\_point-line-sep(eu;P;n) \mmember{} \mBbbP{})
Date html generated:
2020_05_21-AM-10_26_03
Last ObjectModification:
2018_08_11-PM-04_38_29
Theory : euclidean!plane!geometry
Home
Index