### Nuprl Lemma : partition-sum_functionality

`∀I:Interval`
`  (icompact(I)`
`  `` (∀p:partition(I). ∀q:ℝ List.`
`        ((||q|| = ||p|| ∈ ℤ)`
`        `` (∀i:ℕ||q||. (q[i] = p[i]))`
`        `` (∀f:I ⟶ℝ. ∀x:partition-choice(full-partition(I;p)).`
`              (S(f;full-partition(I;p)) = S(f;full-partition(I;q)))))))`

Proof

Definitions occuring in Statement :  partition-sum: `S(f;p)` partition-choice: `partition-choice(p)` full-partition: `full-partition(I;p)` partition: `partition(I)` icompact: `icompact(I)` rfun: `I ⟶ℝ` interval: `Interval` req: `x = y` real: `ℝ` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` all: `∀x:A. B[x]` implies: `P `` Q` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  rev_uimplies: `rev_uimplies(P;Q)` assert: `↑b` bnot: `¬bb` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` cons: `[a / b]` select: `L[n]` less_than': `less_than'(a;b)` le: `A ≤ B` rfun: `I ⟶ℝ` pointwise-req: `x[k] = y[k] for k ∈ [n,m]` icompact: `icompact(I)` subtype_rel: `A ⊆r B` ge: `i ≥ j ` nat: `ℕ` so_apply: `x[s]` partition: `partition(I)` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_lambda: `λ2x.t[x]` guard: `{T}` sq_type: `SQType(T)` prop: `ℙ` and: `P ∧ Q` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` top: `Top` member: `t ∈ T` full-partition: `full-partition(I;p)` partition-sum: `S(f;p)` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  rsub_functionality rmul_functionality req_functionality select-append select-cons-tl less_than_wf assert-bnot bool_subtype_base bool_cases_sqequal eqff_to_assert assert_of_lt_int eqtt_to_assert bool_wf lt_int_wf req_weakening lelt_wf false_wf int_seg_subtype_nat rsub_wf partition-choice-member rmul_wf rsum_functionality nat_wf subtract_wf le_wf int_term_value_subtract_lemma itermSubtract_wf top_wf subtype_rel_list length_append length_cons non_neg_length length_nil nat_properties nil_wf right-endpoint_wf append_wf left-endpoint_wf cons_wf interval_wf icompact_wf partition_wf list_wf length_wf equal_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_le_lemma intformle_wf decidable__le int_seg_properties real_wf select_wf req_wf int_seg_wf all_wf rfun_wf full-partition_wf partition-choice_wf int_subtype_base subtype_base_sq int_formula_prop_wf int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int length_of_nil_lemma length-append length_of_cons_lemma
Rules used in proof :  promote_hyp equalityElimination dependent_set_memberEquality addEquality applyEquality productElimination rename setElimination cumulativity instantiate independent_pairFormation intEquality hypothesisEquality int_eqEquality lambdaEquality dependent_pairFormation independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality equalitySymmetry equalityTransitivity unionElimination because_Cache isectElimination hypothesis voidEquality voidElimination isect_memberEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction sqequalRule cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}I:Interval
(icompact(I)
{}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}q:\mBbbR{}  List.
((||q||  =  ||p||)
{}\mRightarrow{}  (\mforall{}i:\mBbbN{}||q||.  (q[i]  =  p[i]))
{}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}x:partition-choice(full-partition(I;p)).
(S(f;full-partition(I;p))  =  S(f;full-partition(I;q)))))))

Date html generated: 2018_05_22-PM-02_07_59
Last ObjectModification: 2018_05_21-AM-00_21_10

Theory : reals

Home Index