Nuprl Lemma : geo-perp-midsegments
∀e:BasicGeometry. ∀a,b,c:Point. (Rabc ⇒ (∀c',d,p:Point. (c'=p=d ⇒ c'=a=c ⇒ d=b=c ⇒ Rbap)))
Proof
Definitions occuring in Statement :
basic-geometry: BasicGeometry,
right-angle: Rabc,
geo-midpoint: a=m=b,
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],
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
prop: ℙ,
or: P ∨ Q,
basic-geometry: BasicGeometry,
stable: Stable{P},
not: ¬A,
false: False,
geo-eq: a ≡ b,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
exists: ∃x:A. B[x],
geo-midpoint: a=m=b,
geo-cong-tri: Cong3(abc,a'b'c'),
cand: A c∧ B,
uiff: uiff(P;Q),
right-angle: Rabc
Latex:
\mforall{}e:BasicGeometry. \mforall{}a,b,c:Point. (Rabc {}\mRightarrow{} (\mforall{}c',d,p:Point. (c'=p=d {}\mRightarrow{} c'=a=c {}\mRightarrow{} d=b=c {}\mRightarrow{} Rbap)))
Date html generated:
2020_05_20-AM-09_58_30
Last ObjectModification:
2020_01_27-PM-10_00_40
Theory : euclidean!plane!geometry
Home
Index