Nuprl Lemma : mk-eu_wf2

∀[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 ∈ EuclideanPlane 
  supposing BasicGeometryAxioms(self)


Proof



Definitions occuring in Statement :  mk-eu: mk-eu,  euclidean-plane: EuclideanPlane,  circle-strict-overlap: StrictOverlap(a;b;c;d),  basic-geo-axioms: BasicGeometryAxioms(g),  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),  uimplies: b supposing a,  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],  uimplies: b supposing a,  member: t ∈ T,  euclidean-plane: EuclideanPlane,  basic-geo-axioms: BasicGeometryAxioms(g),  geo-lsep: a # bc,  mk-eu: mk-eu,  geo-left: a leftof bc,  geo-sep: a # b,  geo-point: Point,  geo-between: B(abc),  geo-congruent: ab ≅ cd,  geo-gt-prim: ab>cd,  geo-ge: ab ≥ cd,  all: ∀x:A. B[x],  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  bfalse: ff,  geo-length-sep: ab # cd),  subtype_rel: A ⊆r B,  prop: ℙ,  sq_exists: ∃x:A [B[x]],  and: P ∧ Q,  implies: P ⇒ Q,  exists: ∃x:A. B[x],  or: P ∨ Q
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{}  EuclideanPlane 
    supposing  BasicGeometryAxioms(self)


Date html generated: 2020_05_20-AM-10_35_32
Last ObjectModification: 2020_01_29-PM-08_10_19

Theory : euclidean!plane!geometry


Home Index