Nuprl Definition : extra-left-axiom
extra-left-axiom(g) == ∀a,b,c,a':Point. (a_b_a' ⇒ ab ≅ a'b ⇒ ab ≅ cb ⇒ c ≠ a ⇒ c ≠ a' ⇒ a # bc)
Definitions occuring in Statement :
geo-lsep: a # bc,
geo-congruent: ab ≅ cd,
geo-between: a_b_c,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
geo-point: Point,
geo-between: a_b_c,
geo-congruent: ab ≅ cd,
implies: P ⇒ Q,
geo-sep: a ≠ b,
geo-lsep: a # bc
FDL editor aliases :
extra-left-axiom
Latex:
extra-left-axiom(g) ==
\mforall{}a,b,c,a':Point. (a\_b\_a' {}\mRightarrow{} ab \00D0 a'b {}\mRightarrow{} ab \00D0 cb {}\mRightarrow{} c \mneq{} a {}\mRightarrow{} c \mneq{} a' {}\mRightarrow{} a \# bc)
Date html generated:
2017_10_02-PM-03_27_16
Last ObjectModification:
2017_08_09-PM-02_07_47
Theory : euclidean!plane!geometry
Home
Index