interval_average_symm — Mathlib

English

The average over the interval [a,b] equals the average over [b,a] for any function f into a normed space.

Русский

Среднее по интервалу [a,b] равно среднему по [b,a] для любой функции f в нормированном пространстве.

LaTeX

$$$$ \text{average}_{[a,b]} f = \text{average}_{[b,a]} f, $$$$

Lean4

theorem interval_average_symm (f : ℝ → E) (a b : ℝ) : (⨍ x in a..b, f x) = ⨍ x in b..a, f x := by
  rw [setAverage_eq, setAverage_eq, uIoc_comm]

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