integralSum_inf_partition — Mathlib

English

The integral sum over a biUnion with an infimum (prepartition) equals the integral sum over the original partition.

Русский

Сумма интеграла по би-объединению с предразбиением равна сумме по исходному разбиению.

LaTeX

$$$\forall f vol π (π' : Prepartition I) (h : π'.IsPartition)\Rightarrow \mathrm{integralSum} f vol (π.infPrepartition π') = \mathrm{integralSum} f vol π$$$

Lean4

theorem integralSum_inf_partition (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) {π' : Prepartition I}
    (h : π'.IsPartition) : integralSum f vol (π.infPrepartition π') = integralSum f vol π :=
  integralSum_biUnion_partition f vol π _ fun _J hJ => h.restrict (Prepartition.le_of_mem _ hJ)

Похожие утверждения