Nuprl Definition : dist-cong
Dcong(g;a;b;c;d) == (¬D(a;b;b;b;c;d)) ∧ (¬D(c;d;d;d;a;b))
Definitions occuring in Statement :
dist: D(a;b;c;d;e;f),
not: ¬A,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
not: ¬A,
dist: D(a;b;c;d;e;f)
FDL editor aliases :
dist-cong
Latex:
Dcong(g;a;b;c;d) == (\mneg{}D(a;b;b;b;c;d)) \mwedge{} (\mneg{}D(c;d;d;d;a;b))
Date html generated:
2019_10_16-PM-02_46_55
Last ObjectModification:
2018_10_02-AM-11_11_34
Theory : euclidean!plane!geometry
Home
Index