Nuprl Lemma : geo-left_wf

[g:GeometryPrimitives]. ∀[a,b,c:Point].  (a leftof bc ∈ ℙ)


Proof




Definitions occuring in Statement :  geo-left: leftof bc geo-primitives: GeometryPrimitives geo-point: Point uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  prop: so_apply: x[s] so_lambda: λ2x.t[x] btrue: tt ifthenelse: if then else fi  eq_atom: =a y subtype_rel: A ⊆B record-select: r.x record+: record+ geo-left: leftof bc geo-point: Point geo-primitives: GeometryPrimitives member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  geo-primitives_wf geo-point_wf istype-atom top_wf record-select_wf subtype_rel_self
Rules used in proof :  universeIsType isectIsTypeImplies isect_memberEquality_alt inhabitedIsType axiomEquality hypothesisEquality equalitySymmetry equalityTransitivity lambdaEquality_alt cumulativity functionEquality universeEquality isectElimination extract_by_obid instantiate tokenEquality applyEquality hypothesis thin dependentIntersectionEqElimination dependentIntersectionElimination sqequalRule sqequalHypSubstitution cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[g:GeometryPrimitives].  \mforall{}[a,b,c:Point].    (a  leftof  bc  \mmember{}  \mBbbP{})



Date html generated: 2019_10_29-AM-09_12_04
Last ObjectModification: 2019_10_25-PM-01_08_26

Theory : euclidean!plane!geometry


Home Index