Nuprl Definition : geo-left-axioms
geo-left-axioms(g) ==
(∀a,b,c:Point. (¬a # bc ⇐⇒ Colinear(a;b;c)))
∧ (∀a,b,c:Point. (a leftof bc ⇒ b leftof ca))
∧ (∀a,b,c:Point. (a leftof bc ⇒ b ≠ c))
∧ (∀a,b,x,y,z:Point. (x leftof ab ⇒ y leftof ab ⇒ x_z_y ⇒ z # ab))
∧ (∀a,b,c,y:Point. (a # bc ⇒ y ≠ b ⇒ Colinear(y;a;b) ⇒ y # bc))
Definitions occuring in Statement :
geo-lsep: a # bc,
geo-colinear: Colinear(a;b;c),
geo-left: a leftof bc,
geo-between: a_b_c,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q,
geo-left: a leftof bc,
geo-between: a_b_c,
all: ∀x:A. B[x],
geo-point: Point,
geo-sep: a ≠ b,
implies: P ⇒ Q,
geo-colinear: Colinear(a;b;c),
geo-lsep: a # bc
FDL editor aliases :
geo-left-axioms
Latex:
geo-left-axioms(g) ==
(\mforall{}a,b,c:Point. (\mneg{}a \# bc \mLeftarrow{}{}\mRightarrow{} Colinear(a;b;c)))
\mwedge{} (\mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b leftof ca))
\mwedge{} (\mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b \mneq{} c))
\mwedge{} (\mforall{}a,b,x,y,z:Point. (x leftof ab {}\mRightarrow{} y leftof ab {}\mRightarrow{} x\_z\_y {}\mRightarrow{} z \# ab))
\mwedge{} (\mforall{}a,b,c,y:Point. (a \# bc {}\mRightarrow{} y \mneq{} b {}\mRightarrow{} Colinear(y;a;b) {}\mRightarrow{} y \# bc))
Date html generated:
2017_10_02-PM-03_27_13
Last ObjectModification:
2017_08_09-PM-02_08_03
Theory : euclidean!plane!geometry
Home
Index