Nuprl Definition : pgeo-unique
unique(lm,pq) == p I l ⇒ q I l ⇒ p I m ⇒ q I m ⇒ (¬((¬p ≡ q) ∧ (¬l ≡ m)))
Definitions occuring in Statement :
pgeo-leq: a ≡ b,
pgeo-peq: a ≡ b,
pgeo-incident: a I b,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
implies: P ⇒ Q,
pgeo-incident: a I b,
and: P ∧ Q,
pgeo-peq: a ≡ b,
not: ¬A,
pgeo-leq: a ≡ b
FDL editor aliases :
pgeo-unique
Latex:
unique(lm,pq) == p I l {}\mRightarrow{} q I l {}\mRightarrow{} p I m {}\mRightarrow{} q I m {}\mRightarrow{} (\mneg{}((\mneg{}p \mequiv{} q) \mwedge{} (\mneg{}l \mequiv{} m)))
Date html generated:
2018_05_22-PM-00_32_29
Last ObjectModification:
2017_10_30-PM-01_49_27
Theory : euclidean!plane!geometry
Home
Index