stronglyMeasurable_const_smul_iff

English

If c is a unit, then (StronglyMeasurable (c • f)) is equivalent to StronglyMeasurable f.

Русский

Если c является единицей, то (StronglyMeasurable (c • f)) эквивалентно StronglyMeasurable f.

LaTeX

$$$\forall f, \text{IsUnit } c \Rightarrow \Big( \text{StronglyMeasurable (c • f)} \Leftrightarrow \text{StronglyMeasurable } f \Big)$$$

Lean4

nonrec theorem _root_.IsUnit.stronglyMeasurable_const_smul_iff {_ : MeasurableSpace α} {c : M} (hc : IsUnit c) :
    (StronglyMeasurable fun x => c • f x) ↔ StronglyMeasurable f :=
  let ⟨u, hu⟩ := hc
  hu ▸ stronglyMeasurable_const_smul_iff u

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