hasFiniteIntegral_congr — Mathlib

English

If f and g are almost everywhere equal, then HasFiniteIntegral f μ holds if and only if HasFiniteIntegral g μ holds.

Русский

Если f и g равны почти всюду, тогда HasFiniteIntegral f μ выполняется тогда и только тогда, когда HasFiniteIntegral g μ выполняется.

LaTeX

$$$(f =^{\\mathrm{a}}_{\\mu} g) \\Rightarrow (\\HasFiniteIntegral f\\mu \\leftrightarrow \\HasFiniteIntegral g\\mu)$$$

Lean4

theorem hasFiniteIntegral_congr {f g : α → ε} (h : f =ᵐ[μ] g) : HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ :=
  hasFiniteIntegral_congr'_enorm <| h.fun_comp enorm

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