norm_integral_eq_norm_integral_uIoc

English

For any f: ℝ → E, the norm of the integral of f over [a,b] equals the norm of the integral over the half-open interval I a b (which has same measure as [a,b]): ∥∫_{a}^{b} f x dμ∥ = ∥∫_{Ι a b} f x dμ∥.

Русский

Для любой f: ℝ → E, норма интеграла по [a,b] равна норме интеграла по полузакрытому интервалу I a b: ∥∫_{a}^{b} f(x) dx∥ = ∥∫_{Ι a b} f(x) dx∥.

LaTeX

$$$\|\int_{a}^{b} f(x) \, d\mu\| = \|\int_{Ι a b} f(x) \, d\mu\|$$$

Lean4

theorem norm_integral_eq_norm_integral_uIoc (f : ℝ → E) : ‖∫ x in a..b, f x ∂μ‖ = ‖∫ x in Ι a b, f x ∂μ‖ := by
  rw [← norm_integral_min_max, integral_of_le min_le_max, uIoc]

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