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