abs — Mathlib

English

If f is CircleIntegrable, then its absolute value |f| is CircleIntegrable.

Русский

Если f CircleIntegrable, то |f| CircleIntegrable.

LaTeX

$$$\text{CircleIntegrable}(f,c,R) \Rightarrow \text{CircleIntegrable}(|f|,c,R).$$$

Lean4

/-- Analogue of `IntervalIntegrable.abs`: If a real-valued function `f` is circle integrable, then so is
`|f|`.
-/
theorem abs {f : ℂ → ℝ} (hf : CircleIntegrable f c R) : CircleIntegrable |f| c R :=
  IntervalIntegrable.abs hf

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