measurableSMul₂_opposite_of_mul

English

For GroupWithZero G₀, if c ≠ 0, then Measurable (λ x, c • f x) is equivalent to Measurable f.

Русский

Для GroupWithZero G₀, при c ≠ 0 измеримость функций сохраняется: Measurable(λx, c•f x) ↔ Measurable f.

LaTeX

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

Lean4

@[to_additive]
instance measurableSMul₂_opposite_of_mul {M : Type*} [Mul M] [MeasurableSpace M] [MeasurableMul₂ M] :
    MeasurableSMul₂ Mᵐᵒᵖ M :=
  ⟨measurable_snd.mul (measurable_mul_unop.comp measurable_fst)⟩

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