Nuprl Lemma : in-hull-unique2

[g:OrientedPlane]. ∀[xs:{xs:Point List| geo-general-position(g;xs)} ]. ∀[i,j,k:ℕ||xs||].
  (j k ∈ ℤsupposing (ki ∈ Hull(xs) and (k i ∈ ℤ)) and ji ∈ Hull(xs) and (j i ∈ ℤ)))


Proof




Definitions occuring in Statement :  in-hull: ij ∈ Hull(xs) geo-general-position: geo-general-position(g;xs) oriented-plane: OrientedPlane geo-point: Point length: ||as|| list: List int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] not: ¬A set: {x:A| B[x]}  natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  so_apply: x[s] so_lambda: λ2x.t[x] prop: top: Top false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) and: P ∧ Q lelt: i ≤ j < k subtype_rel: A ⊆B guard: {T} not: ¬A implies:  Q in-hull: ij ∈ Hull(xs) or: P ∨ Q decidable: Dec(P) int_seg: {i..j-} all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] uiff: uiff(P;Q) cand: c∧ B btrue: tt ifthenelse: if then else fi  bnot: ¬bb
Lemmas referenced :  list_wf set_wf int_seg_wf not_wf Error :geo-primitives_wf,  Error :geo-structure_wf,  Error :oriented-plane_wf,  subtype_rel_transitivity Error :oriented-plane_subtype,  Error :real-geometry-subtype,  Error :geo-structure-subtype-primitives,  geo-general-position_wf in-hull_wf equal_wf int_formula_prop_wf int_formula_prop_not_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformnot_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt Error :geo-point_wf,  length_wf int_seg_properties decidable__equal_int bnot-left-test bnot_wf left-test-symmetry left-test_wf assert_functionality_wrt_uiff btrue_neq_bfalse bool_wf and_wf bfalse_wf assert_elim assert_of_bnot
Rules used in proof :  equalitySymmetry equalityTransitivity axiomEquality instantiate dependent_set_memberEquality computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality lambdaEquality dependent_pairFormation independent_isectElimination productElimination sqequalRule applyEquality natural_numberEquality isectElimination lambdaFormation independent_functionElimination hypothesisEquality unionElimination hypothesis because_Cache rename setElimination thin dependent_functionElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productEquality applyLambdaEquality

Latex:
\mforall{}[g:OrientedPlane].  \mforall{}[xs:\{xs:Point  List|  geo-general-position(g;xs)\}  ].  \mforall{}[i,j,k:\mBbbN{}||xs||].
    (j  =  k)  supposing  (ki  \mmember{}  Hull(xs)  and  (\mneg{}(k  =  i))  and  ji  \mmember{}  Hull(xs)  and  (\mneg{}(j  =  i)))



Date html generated: 2017_10_02-PM-06_51_56
Last ObjectModification: 2017_08_06-PM-07_31_40

Theory : euclidean!plane!geometry


Home Index