Nuprl Definition : pgeo-lsep-class
pgeo-lsep-class(g;m;n) == ∃l',l:Line. ((l' = m ∈ LineClass) ∧ (l = n ∈ LineClass) ∧ l' ≠ l)
Definitions occuring in Statement :
pgeo-line-class: LineClass,
pgeo-lsep: l ≠ m,
pgeo-line: Line,
exists: ∃x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
pgeo-line: Line,
and: P ∧ Q,
equal: s = t ∈ T,
pgeo-line-class: LineClass,
pgeo-lsep: l ≠ m
FDL editor aliases :
pgeo-lsep-class
Latex:
pgeo-lsep-class(g;m;n) == \mexists{}l',l:Line. ((l' = m) \mwedge{} (l = n) \mwedge{} l' \mneq{} l)
Date html generated:
2018_05_22-PM-00_57_14
Last ObjectModification:
2018_01_03-PM-04_16_26
Theory : euclidean!plane!geometry
Home
Index