Nuprl Definition : eu-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 :
eu-cong-tri: Cong3(abc,a'b'c'),
eu-colinear: Colinear(a;b;c),
eu-congruent: ab=cd,
and: P ∧ Q
Definitions occuring in definition :
eu-colinear: Colinear(a;b;c),
eu-cong-tri: Cong3(abc,a'b'c'),
and: P ∧ Q,
eu-congruent: ab=cd
FDL editor aliases :
eu-fsc
Latex:
FSC(a;b;c;d a';b';c';d') == Colinear(a;b;c) \mwedge{} Cong3(abc,a'b'c') \mwedge{} ad=a'd' \mwedge{} bd=b'd'
Date html generated:
2016_05_18-AM-06_42_06
Last ObjectModification:
2015_09_23-AM-09_00_25
Theory : euclidean!geometry
Home
Index