Nuprl Definition : geo-five-seg-compressed
FSC(a;b;c;d a';b';c';d') == Colinear(a;b;c) ∧ Cong3(abc,a'b'c') ∧ ad ≅ a'd' ∧ bd ≅ b'd'
Definitions occuring in Statement :
geo-cong-tri: Cong3(abc,a'b'c'),
geo-colinear: Colinear(a;b;c),
geo-congruent: ab ≅ cd,
and: P ∧ Q
Definitions occuring in definition :
geo-colinear: Colinear(a;b;c),
geo-cong-tri: Cong3(abc,a'b'c'),
and: P ∧ Q,
geo-congruent: ab ≅ cd
FDL editor aliases :
eu-fsc
eu-fsc
Latex:
FSC(a;b;c;d a';b';c';d') == Colinear(a;b;c) \mwedge{} Cong3(abc,a'b'c') \mwedge{} ad \00D0 a'd' \mwedge{} bd \00D0 b'd'
Date html generated:
2017_10_02-PM-06_31_28
Last ObjectModification:
2017_08_05-PM-04_42_30
Theory : euclidean!plane!geometry
Home
Index