Nuprl Lemma : geo-colinear-left-out
∀e:EuclideanPlane. ∀a,b,x,y:Point. (Colinear(b;x;y) ⇒ x leftof ab ⇒ y leftof ab ⇒ out(b xy))
Proof
Definitions occuring in Statement :
geo-out: out(p ab),
euclidean-plane: EuclideanPlane,
geo-colinear: Colinear(a;b;c),
geo-left: a leftof bc,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
geo-out: out(p ab),
and: P ∧ Q,
member: t ∈ T,
guard: {T},
cand: A c∧ B,
not: ¬A,
basic-geometry-: BasicGeometry-,
uall: ∀[x:A]. B[x],
geo-eq: a ≡ b,
subtype_rel: A ⊆r B,
prop: ℙ,
uimplies: b supposing a,
oriented-plane: OrientedPlane,
false: False,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
geo-strict-between: a-b-c
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,x,y:Point. (Colinear(b;x;y) {}\mRightarrow{} x leftof ab {}\mRightarrow{} y leftof ab {}\mRightarrow{} out(b xy))
Date html generated:
2020_05_20-AM-09_56_28
Last ObjectModification:
2019_12_23-PM-08_44_23
Theory : euclidean!plane!geometry
Home
Index