Nuprl Lemma : eu-colinear-is-colinear-set

`∀e:EuclideanPlane. ∀A,B,C:Point.  (Colinear(A;B;C) `` eu-colinear-set(e;[A; B; C]))`

Proof

Definitions occuring in Statement :  eu-colinear-set: `eu-colinear-set(e;L)` euclidean-plane: `EuclideanPlane` eu-colinear: `Colinear(a;b;c)` eu-point: `Point` cons: `[a / b]` nil: `[]` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` eu-colinear-set: `eu-colinear-set(e;L)` l_all: `(∀x∈L.P[x])` member: `t ∈ T` top: `Top` int_seg: `{i..j-}` decidable: `Dec(P)` or: `P ∨ Q` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` sq_type: `SQType(T)` guard: `{T}` select: `L[n]` cons: `[a / b]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` cand: `A c∧ B` nat: `ℕ` not: `¬A` false: `False` subtract: `n - m` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` le: `A ≤ B` less_than': `less_than'(a;b)` lelt: `i ≤ j < k` stable: `Stable{P}`
Lemmas referenced :  length_of_cons_lemma length_of_nil_lemma decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties l_all_iff cons_wf eu-point_wf nil_wf l_member_wf l_all_wf2 not_wf equal_wf eu-colinear_wf eu-colinear-def member_wf eu-between_wf nat_properties satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_subtype false_wf int_seg_cases eu-colinear-swap eu-colinear-cycle eu-colinear-permute int_seg_wf length_wf euclidean-plane_wf stable__colinear or_wf minimal-double-negation-hyp-elim minimal-not-not-excluded-middle
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution sqequalRule cut introduction extract_by_obid dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis setElimination rename hypothesisEquality natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination equalityTransitivity equalitySymmetry lambdaEquality functionEquality setEquality productElimination independent_pairFormation productEquality dependent_pairFormation int_eqEquality computeAll hyp_replacement Error :applyLambdaEquality,  hypothesis_subsumption addEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C:Point.    (Colinear(A;B;C)  {}\mRightarrow{}  eu-colinear-set(e;[A;  B;  C]))

Date html generated: 2016_10_26-AM-07_43_33
Last ObjectModification: 2016_07_12-AM-08_11_07

Theory : euclidean!geometry

Home Index