inter_of_restrict — Mathlib

English

If there is an equality almost everywhere of f and g on s, then IntegrableOn f s μ iff IntegrableOn g s μ.

Русский

Если f и g равны почти всюду на s, то IntegrableOn f s μ эквивалентно IntegrableOn g s μ.

LaTeX

$$$(\mathrm{ae}(\mu|_s)).\mathrm{EventuallyEq} f g \to \mathrm{IntegrableOn}(f,s,\mu) \iff \mathrm{IntegrableOn}(g,s,\mu)$$$

Lean4

theorem inter_of_restrict (h : IntegrableOn f s (μ.restrict t)) : IntegrableOn f (s ∩ t) μ :=
  by
  have := h.mono_set (inter_subset_left (t := t))
  rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this

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