Nuprl Lemma : Euclid-Prop23

e:EuclideanPlane. ∀a,b,x,y,z:Point.  (z xy   (∃x',b':Point. (out(a bb') ∧ x' ab' ∧ x'ab' ≅a zxy)))


Proof




Definitions occuring in Statement :  geo-out: out(p ab) geo-cong-angle: abc ≅a xyz euclidean-plane: EuclideanPlane geo-lsep: bc geo-sep: b geo-point: Point all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T guard: {T} and: P ∧ Q cand: c∧ B exists: x:A. B[x] uall: [x:A]. B[x] euclidean-plane: EuclideanPlane sq_stable: SqStable(P) squash: T geo-out: out(p ab) subtype_rel: A ⊆B prop: uimplies: supposing a basic-geometry: BasicGeometry geo-cong-angle: abc ≅a xyz uiff: uiff(P;Q)

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y,z:Point.
    (z  \#  xy  {}\mRightarrow{}  a  \#  b  {}\mRightarrow{}  (\mexists{}x',b':Point.  (out(a  bb')  \mwedge{}  x'  \#  ab'  \mwedge{}  x'ab'  \mcong{}\msuba{}  zxy)))



Date html generated: 2020_05_20-AM-10_40_26
Last ObjectModification: 2020_01_13-PM-05_30_32

Theory : euclidean!plane!geometry


Home Index