Nuprl Lemma : point-perspective_wf
∀g:ProjectivePlane. ∀a,b,c,A,B,C,o:Point. (pPerspective(PΔ(a;b;c);PΔ(A;B;C);o) ∈ ℙ)
Proof
Definitions occuring in Statement :
point-perspective: pPerspective(PΔ(a;b;c);PΔ(A;B;C);o),
projective-plane: ProjectivePlane,
pgeo-point: Point,
prop: ℙ,
all: ∀x:A. B[x],
member: t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
point-perspective: pPerspective(PΔ(a;b;c);PΔ(A;B;C);o),
prop: ℙ,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
pgeo-triangle: pgeo-triangle(pg),
guard: {T},
uimplies: b supposing a
Latex:
\mforall{}g:ProjectivePlane. \mforall{}a,b,c,A,B,C,o:Point. (pPerspective(P\mDelta{}(a;b;c);P\mDelta{}(A;B;C);o) \mmember{} \mBbbP{})
Date html generated:
2020_05_20-AM-10_37_38
Last ObjectModification:
2020_01_13-PM-06_17_01
Theory : euclidean!plane!geometry
Home
Index