Nuprl Definition : pgeo-plsep-class
pc # lc == ∃p:Point. ∃l:Line. ((p = pc ∈ PointClass) ∧ (l = lc ∈ LineClass) ∧ p ≠ l)
Definitions occuring in Statement :
pgeo-line-class: LineClass,
pgeo-point-class: PointClass,
pgeo-plsep: a ≠ b,
pgeo-line: Line,
pgeo-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
pgeo-point: Point,
exists: ∃x:A. B[x],
pgeo-line: Line,
pgeo-point-class: PointClass,
and: P ∧ Q,
equal: s = t ∈ T,
pgeo-line-class: LineClass,
pgeo-plsep: a ≠ b
FDL editor aliases :
pgeo-plsep-class
Latex:
pc \# lc == \mexists{}p:Point. \mexists{}l:Line. ((p = pc) \mwedge{} (l = lc) \mwedge{} p \mneq{} l)
Date html generated:
2018_05_22-PM-00_56_33
Last ObjectModification:
2018_01_03-PM-03_47_14
Theory : euclidean!plane!geometry
Home
Index