Nuprl Definition : pgeo-line-class
LineClass ==  l,m:Line//l ≡ m
Definitions occuring in Statement : 
pgeo-leq: a ≡ b
, 
pgeo-line: Line
, 
quotient: x,y:A//B[x; y]
Definitions occuring in definition : 
quotient: x,y:A//B[x; y]
, 
pgeo-line: Line
, 
pgeo-leq: a ≡ b
FDL editor aliases : 
pgeo-line-class
Latex:
LineClass  ==    l,m:Line//l  \mequiv{}  m
Date html generated:
2018_05_22-PM-00_56_13
Last ObjectModification:
2018_01_03-PM-03_42_49
Theory : euclidean!plane!geometry
Home
Index