Nuprl Lemma : q-linear-times

[X:ℕ ⟶ ℚ]. ∀[a:ℚ]. ∀[k:ℕ]. ∀[y:ℚ List].  q-linear(k;j.a X[j];y) (a q-linear(k;j.X[j];y)) ∈ ℚ supposing k ≤ ||y||


Proof




Definitions occuring in Statement :  q-linear: q-linear(k;i.X[i];y) qmul: s rationals: length: ||as|| list: List nat: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A all: x:A. B[x] top: Top and: P ∧ Q prop: squash: T so_lambda: λ2x.t[x] so_apply: x[s] le: A ≤ B less_than': less_than'(a;b) true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P) or: P ∨ Q nat_plus: +
Lemmas referenced :  nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf le_wf length_wf rationals_wf list_wf equal_wf squash_wf true_wf q-linear-base qmul_wf nat_wf q-linear_wf false_wf iff_weakening_equal decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma select_wf decidable__lt qadd_wf q-linear-unroll qmul_over_plus_qrng qmul_assoc_qrng qmul_comm_qrng qmul_ac_1_qrng qadd_comm_q
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry applyEquality imageElimination universeEquality functionExtensionality dependent_set_memberEquality imageMemberEquality baseClosed productElimination because_Cache unionElimination functionEquality

Latex:
\mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[a:\mBbbQ{}].  \mforall{}[k:\mBbbN{}].  \mforall{}[y:\mBbbQ{}  List].
    q-linear(k;j.a  *  X[j];y)  =  (a  *  q-linear(k;j.X[j];y))  supposing  k  \mleq{}  ||y||



Date html generated: 2018_05_22-AM-00_17_41
Last ObjectModification: 2017_07_26-PM-06_53_36

Theory : rationals


Home Index