congr — Mathlib

English

If f and g are equal almost everywhere and f is integrable, then g is integrable; conversely, if g is integrable then f is.

Русский

Если f = g почти всюду и f интегрируема, то и g интегрируема; наоборот, если g интегрируема, то и f.

LaTeX

$$$\operatorname{Integrable}(f, \mu) \to (f =^{\mathrm{ae}} g) \Rightarrow \operatorname{Integrable}(g, \mu)$$$

Lean4

theorem congr {f g : α → ε} (hf : Integrable f μ) (h : f =ᵐ[μ] g) : Integrable g μ :=
  ⟨hf.1.congr h, hf.2.congr h⟩

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