Nuprl Lemma : Dbet-to-between
∀e:EuclideanPlane. ∀a,b,c:Point. ((∀A,B,C:Point. (A # BC ⇒ |AC| < |AB| + |BC|)) ⇒ Dbet(e;a;b;c) ⇒ B(abc))
Proof
Definitions occuring in Statement :
dist-bet: Dbet(g;a;b;c),
geo-lt: p < q,
geo-add-length: p + q,
geo-length: |s|,
geo-mk-seg: ab,
euclidean-plane: EuclideanPlane,
geo-between: B(abc),
geo-lsep: a # bc,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
basic-geometry: BasicGeometry,
euclidean-plane: EuclideanPlane,
or: P ∨ Q,
not: ¬A,
false: False,
stable: Stable{P},
iff: P ⇐⇒ Q,
and: P ∧ Q,
basic-geometry-: BasicGeometry-,
rev_implies: P ⇐ Q,
geo-strict-between: a-b-c,
uiff: uiff(P;Q),
squash: ↓T,
true: True
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c:Point.
((\mforall{}A,B,C:Point. (A \# BC {}\mRightarrow{} |AC| < |AB| + |BC|)) {}\mRightarrow{} Dbet(e;a;b;c) {}\mRightarrow{} B(abc))
Date html generated:
2020_05_20-AM-10_48_52
Last ObjectModification:
2020_01_13-PM-06_50_12
Theory : euclidean!plane!geometry
Home
Index