Nuprl Definition : dist-axiomsA
dist-axiomsA(g) ==
(∀a,b,c,d,e,f,h:Point. (D(a;b;c;d;e;f) ⇒ D(a;b;c;d;h;h)))
∧ (∀a,b,c,d,e,f:Point. (D(a;b;c;c;e;f) ⇒ D(a;b;d;d;e;f)))
∧ (∀a,b,c,d,e,f:Point. (D(a;b;c;d;e;f) ⇒ (D(b;a;c;d;e;f) ∧ D(a;b;c;d;f;e))))
∧ (∀a,b,c,d,e,f:Point. (D(a;b;c;d;e;f) ⇒ D(c;d;a;b;e;f)))
∧ (∀a,b,c,d:Point. (D(a;b;b;b;c;d) ⇒ (¬D(c;d;d;d;a;b))))
∧ (∀a,b,c,d,e,f,x,y:Point. ((D(a;b;c;d;e;f) ∧ (¬D(x;y;y;y;e;f))) ⇒ D(a;b;c;d;x;y)))
∧ (∀a,b,c,d,e,f,x,y:Point. ((D(a;b;c;d;e;f) ∧ (¬D(a;b;b;b;x;y))) ⇒ D(x;y;c;d;e;f)))
∧ (∀a,b,c,d,e,f:Point. (D(a;b;b;b;c;d) ⇒ (D(a;b;b;b;e;f) ∨ D(e;f;f;f;c;d))))
Definitions occuring in Statement :
dist: D(a;b;c;d;e;f),
geo-point: Point,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q
Definitions occuring in definition :
dist: D(a;b;c;d;e;f),
and: P ∧ Q,
implies: P ⇒ Q,
geo-point: Point,
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q
FDL editor aliases :
dist-axiomsA
Latex:
dist-axiomsA(g) ==
(\mforall{}a,b,c,d,e,f,h:Point. (D(a;b;c;d;e;f) {}\mRightarrow{} D(a;b;c;d;h;h)))
\mwedge{} (\mforall{}a,b,c,d,e,f:Point. (D(a;b;c;c;e;f) {}\mRightarrow{} D(a;b;d;d;e;f)))
\mwedge{} (\mforall{}a,b,c,d,e,f:Point. (D(a;b;c;d;e;f) {}\mRightarrow{} (D(b;a;c;d;e;f) \mwedge{} D(a;b;c;d;f;e))))
\mwedge{} (\mforall{}a,b,c,d,e,f:Point. (D(a;b;c;d;e;f) {}\mRightarrow{} D(c;d;a;b;e;f)))
\mwedge{} (\mforall{}a,b,c,d:Point. (D(a;b;b;b;c;d) {}\mRightarrow{} (\mneg{}D(c;d;d;d;a;b))))
\mwedge{} (\mforall{}a,b,c,d,e,f,x,y:Point. ((D(a;b;c;d;e;f) \mwedge{} (\mneg{}D(x;y;y;y;e;f))) {}\mRightarrow{} D(a;b;c;d;x;y)))
\mwedge{} (\mforall{}a,b,c,d,e,f,x,y:Point. ((D(a;b;c;d;e;f) \mwedge{} (\mneg{}D(a;b;b;b;x;y))) {}\mRightarrow{} D(x;y;c;d;e;f)))
\mwedge{} (\mforall{}a,b,c,d,e,f:Point. (D(a;b;b;b;c;d) {}\mRightarrow{} (D(a;b;b;b;e;f) \mvee{} D(e;f;f;f;c;d))))
Date html generated:
2019_10_16-PM-02_44_30
Last ObjectModification:
2018_09_14-AM-09_35_41
Theory : euclidean!plane!geometry
Home
Index