Nuprl Lemma : mk-eu_wf

∀[self:GeometryPrimitives]. ∀[Sstab:∀a,b,c,d:Point.  SqStable(ab>cd)]. ∀[Lstab:∀a,b,c:Point.  SqStable(a # bc)].
∀[Sepor:∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.  (a # c ∨ b # c)]. ∀[nontriv:∃a:Point. (∃b:Point [a # b])].
∀[SS:∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:Point [(Colinear(a;b;x) ∧ B(uxv))])].
∀[SC:∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} .  (∃u:Point [(cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u))])].
∀[CC:∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:{d:Point| StrictOverlap(a;b;c;d)} .
       (∃u:Point [(ab ≅ au ∧ cd ≅ cu ∧ u leftof ac)])].
  (primitive=self
   Ssquashstable=Sstab
   Lorsquashstable=Lstab
   SepOr=Sepor
   nontriv=nontriv
   SS=SS
   SC=SC
   CC=CC ∈ EuclideanPlaneStructure)


Proof



Definitions occuring in Statement :  mk-eu: mk-eu,  euclidean-plane-structure: EuclideanPlaneStructure,  circle-strict-overlap: StrictOverlap(a;b;c;d),  geo-colinear: Colinear(a;b;c),  geo-congruent: ab ≅ cd,  geo-between: B(abc),  geo-lsep: a # bc,  geo-left: a leftof bc,  geo-sep: a # b,  geo-gt-prim: ab>cd,  geo-primitives: GeometryPrimitives,  geo-point: Point,  sq_stable: SqStable(P),  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} 
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  mk-eu: mk-eu,  euclidean-plane-structure: EuclideanPlaneStructure,  record+: record+,  record-update: r[x := v],  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  subtype_rel: A ⊆r B,  uiff: uiff(P;Q),  and: P ∧ Q,  uimplies: b supposing a,  ifthenelse: if b then t else f fi ,  sq_type: SQType(T),  guard: {T},  record-select: r.x,  geo-gt-prim: ab>cd,  geo-point: Point,  eq_atom: x =a y,  bfalse: ff,  iff: P ⇐⇒ Q,  not: ¬A,  rev_implies: P ⇐ Q,  false: False,  geo-left: a leftof bc,  geo-lsep: a # bc,  geo-sep: a # b,  geo-between: B(abc),  geo-colinear: Colinear(a;b;c),  geo-congruent: ab ≅ cd,  geo-length-sep: ab # cd),  circle-strict-overlap: StrictOverlap(a;b;c;d),  prop: ℙ,  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  or: P ∨ Q,  geo-primitives: GeometryPrimitives,  record: record(x.T[x])
Latex:
\mforall{}[self:GeometryPrimitives].  \mforall{}[Sstab:\mforall{}a,b,c,d:Point.    SqStable(ab>cd)].  \mforall{}[Lstab:\mforall{}a,b,c:Point.
                                                                                                                                                                  SqStable(a  \#  bc)].
\mforall{}[Sepor:\mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:Point.    (a  \#  c  \mvee{}  b  \#  c)].  \mforall{}[nontriv:\mexists{}a:Point
                                                                                                                                                              (\mexists{}b:Point  [a  \#  b])].
\mforall{}[SS:\mforall{}a,b:Point.  \mforall{}u:\{u:Point|  u  leftof  ab\}  .  \mforall{}v:\{v:Point|  v  leftof  ba\}  .
              (\mexists{}x:Point  [(Colinear(a;b;x)  \mwedge{}  B(uxv))])].  \mforall{}[SC:\mforall{}c,d,a:Point.  \mforall{}b:\{b:Point|  b  \#  a  \mwedge{}  B(cbd)\}  .
                                                                                                                (\mexists{}u:Point  [(cu  \mcong{}  cd
                                                                                                                                    \mwedge{}  B(abu)
                                                                                                                                    \mwedge{}  (b  \#  d  {}\mRightarrow{}  b  \#  u))])].
\mforall{}[CC:\mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  c\}  .  \mforall{}d:\{d:Point|  StrictOverlap(a;b;c;d)\}  .
              (\mexists{}u:Point  [(ab  \mcong{}  au  \mwedge{}  cd  \mcong{}  cu  \mwedge{}  u  leftof  ac)])].
    (primitive=self
      Ssquashstable=Sstab
      Lorsquashstable=Lstab
      SepOr=Sepor
      nontriv=nontriv
      SS=SS
      SC=SC
      CC=CC  \mmember{}  EuclideanPlaneStructure)


Date html generated: 2020_05_20-AM-10_35_18
Last ObjectModification: 2020_01_29-PM-04_28_10

Theory : euclidean!plane!geometry


Home Index