aestronglyMeasurable_const_smul_iff

English

For any scalar c in a topological field, AEStronglyMeasurable (c • f) μ is equivalent to AEStronglyMeasurable f μ.

Русский

Для любого скаляра c в топологическом поле AEStronglyMeasurable (c • f) μ эквивалентно AEStronglyMeasurable f μ.

LaTeX

$$$\text{AEStronglyMeasurable}(c \cdot f, μ) \iff \text{AEStronglyMeasurable}(f, μ).$$$

Lean4

theorem _root_.aestronglyMeasurable_const_smul_iff (c : G) :
    AEStronglyMeasurable (fun x => c • f x) μ ↔ AEStronglyMeasurable f μ :=
  ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul' c⁻¹, fun h => h.const_smul c⟩

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