Nuprl Definition : line-perspective
LPerspective(LΔ(l;m;n);LΔ(L;M;N);y) ==
∀l,m,n,L,M,N,y:Line. ∀s1:l ≠ L. ∀s2:m ≠ M. ∀s3:n ≠ N. ((LΔ(l;m;n) ∧ LΔ(L;M;N)) ∧ (l ∧ L I y ∧ m ∧ M I y) ∧ n ∧ N I y)
Definitions occuring in Statement :
line-triangle: LΔ(l;m;n),
pgeo-meet: l ∧ m,
pgeo-lsep: l ≠ m,
pgeo-incident: a I b,
pgeo-line: Line,
all: ∀x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
pgeo-line: Line,
all: ∀x:A. B[x],
pgeo-lsep: l ≠ m,
line-triangle: LΔ(l;m;n),
and: P ∧ Q,
pgeo-incident: a I b,
pgeo-meet: l ∧ m
FDL editor aliases :
line-perspective
Latex:
LPerspective(L\mDelta{}(l;m;n);L\mDelta{}(L;M;N);y) ==
\mforall{}l,m,n,L,M,N,y:Line. \mforall{}s1:l \mneq{} L. \mforall{}s2:m \mneq{} M. \mforall{}s3:n \mneq{} N.
((L\mDelta{}(l;m;n) \mwedge{} L\mDelta{}(L;M;N)) \mwedge{} (l \mwedge{} L I y \mwedge{} m \mwedge{} M I y) \mwedge{} n \mwedge{} N I y)
Date html generated:
2018_05_22-PM-00_51_59
Last ObjectModification:
2017_12_01-PM-00_00_57
Theory : euclidean!plane!geometry
Home
Index