sub' — Mathlib

English

If f is integrable, then the norm ‖f‖ is integrable; conversely, if ‖f‖ is integrable, then f is integrable.

Русский

Если f интегрируемо, то ‖f‖ интегрируемо; и наоборот.

LaTeX

$$$ (AEStronglyMeasurable\\ f\\ μ) \\Rightarrow (Integrable\\ f\\ μ \\iff Integrable(\\|f\\|)\\ μ) $$$

Lean4

@[fun_prop]
theorem sub' {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) : Integrable (fun a ↦ f a - g a) μ := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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