measurable_const_smul_iff — Mathlib

English

For a fixed group element c acting on a space with a measurable G-action, the map x ↦ c • f x is measurable iff f is measurable.

Русский

Для фиксированного элемента группы c и действия на пространстве с измеримой функцией, отображение x ↦ c • f(x) измеримо тогда и только тогда, когда f измерима.

LaTeX

$$$\text{Measurable } (\lambda x. c \cdot f(x)) \iff \text{Measurable } f$$$

Lean4

@[to_additive]
theorem measurable_const_smul_iff (c : G) : (Measurable fun x => c • f x) ↔ Measurable f :=
  ⟨fun h => by simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹, fun h => h.const_smul c⟩

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