Nuprl Definition : dist-axiomsB

dist-axiomsB(g) ==
  (∀a,b,c,d:Point.  ((Dbet(g;a;b;c) ∧ Dbet(g;a;c;d)) ⇒ Dbet(g;b;c;d)))
  ∧ (∀a,b,c,d:Point.  ((Dbet(g;a;b;d) ∧ Dbet(g;b;c;d)) ⇒ Dbet(g;a;c;d)))
  ∧ (∀a,b,c,d:Point.  (((Dsep(g;b;c) ∧ Dbet(g;a;b;c)) ∧ Dbet(g;b;c;d)) ⇒ Dbet(g;a;b;d)))
  ∧ (∀a,b,c:Point.  ((Dbet(g;a;b;c) ∧ Dsep(g;b;c)) ⇒ D(a;c;c;c;a;b)))
  ∧ (∀a,b,c,d:Point.
       (((Dbet(g;a;b;c) ∧ Dbet(g;a;b;d)) ∧ Dsep(g;a;b) ∧ Dsep(g;c;d)) ⇒ (Dbet(g;a;c;d) ∨ Dbet(g;a;d;c))))
  ∧ (∀a,b,c,d,e:Point.  (Dbet(g;a;b;c) ⇒ (D(a;b;b;c;d;e) ⇐⇒ D(a;c;c;c;d;e))))
  ∧ (∀a,b,c,x:Point.  (Dtri(g;a;b;c) ⇒ (Dsep(g;c;x) ∨ Dtri(g;a;b;x))))


Definitions occuring in Statement :  dist-bet: Dbet(g;a;b;c),  dist-tri: Dtri(g;a;b;c),  dist-sep: Dsep(g;a;b),  dist: D(a;b;c;d;e;f),  geo-point: Point,  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q
Definitions occuring in definition :  implies: P ⇒ Q,  geo-point: Point,  all: ∀x:A. B[x],  dist: D(a;b;c;d;e;f),  iff: P ⇐⇒ Q,  dist-bet: Dbet(g;a;b;c),  and: P ∧ Q,  or: P ∨ Q,  dist-sep: Dsep(g;a;b),  dist-tri: Dtri(g;a;b;c)
FDL editor aliases :  dist-axiomsB
Latex:
dist-axiomsB(g)  ==
    (\mforall{}a,b,c,d:Point.    ((Dbet(g;a;b;c)  \mwedge{}  Dbet(g;a;c;d))  {}\mRightarrow{}  Dbet(g;b;c;d)))
    \mwedge{}  (\mforall{}a,b,c,d:Point.    ((Dbet(g;a;b;d)  \mwedge{}  Dbet(g;b;c;d))  {}\mRightarrow{}  Dbet(g;a;c;d)))
    \mwedge{}  (\mforall{}a,b,c,d:Point.    (((Dsep(g;b;c)  \mwedge{}  Dbet(g;a;b;c))  \mwedge{}  Dbet(g;b;c;d))  {}\mRightarrow{}  Dbet(g;a;b;d)))
    \mwedge{}  (\mforall{}a,b,c:Point.    ((Dbet(g;a;b;c)  \mwedge{}  Dsep(g;b;c))  {}\mRightarrow{}  D(a;c;c;c;a;b)))
    \mwedge{}  (\mforall{}a,b,c,d:Point.
              (((Dbet(g;a;b;c)  \mwedge{}  Dbet(g;a;b;d))  \mwedge{}  Dsep(g;a;b)  \mwedge{}  Dsep(g;c;d))
              {}\mRightarrow{}  (Dbet(g;a;c;d)  \mvee{}  Dbet(g;a;d;c))))
    \mwedge{}  (\mforall{}a,b,c,d,e:Point.    (Dbet(g;a;b;c)  {}\mRightarrow{}  (D(a;b;b;c;d;e)  \mLeftarrow{}{}\mRightarrow{}  D(a;c;c;c;d;e))))
    \mwedge{}  (\mforall{}a,b,c,x:Point.    (Dtri(g;a;b;c)  {}\mRightarrow{}  (Dsep(g;c;x)  \mvee{}  Dtri(g;a;b;x))))


Date html generated: 2019_10_16-PM-02_47_32
Last ObjectModification: 2018_09_14-PM-09_03_40

Theory : euclidean!plane!geometry


Home Index