Nuprl Lemma : geo-left-out-better

e:EuclideanPlane. ∀a,b,a',p:Point.  (p leftof ba  a'  ((¬B(baa')) ∧ B(ba'a))))  leftof ba')


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane geo-between: B(abc) geo-left: leftof bc geo-sep: b geo-point: Point all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q geo-lsep: bc or: P ∨ Q member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B prop: geo-colinear: Colinear(a;b;c) not: ¬A and: P ∧ Q cand: c∧ B uimplies: supposing a geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False select: L[n] cons: [a b] subtract: m guard: {T} iff: ⇐⇒ Q

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,a',p:Point.
    (p  leftof  ba  {}\mRightarrow{}  b  \#  a'  {}\mRightarrow{}  (\mneg{}((\mneg{}B(baa'))  \mwedge{}  (\mneg{}B(ba'a))))  {}\mRightarrow{}  p  leftof  ba')



Date html generated: 2020_05_20-AM-09_56_11
Last ObjectModification: 2019_12_23-PM-08_44_39

Theory : euclidean!plane!geometry


Home Index