measurableSMul_nat₂ — Mathlib

English

If each component α_i has a SMul M, then the Pi-type ∀ i, α_i has a MeasurableSMul M.

Русский

Если каждый компонент пространства α_i имеет SMul от M, то π-тип ∀ i, α_i имеет MeasurableSMul от M.

LaTeX

$$$\text{MeasurableSMul } M ((i: I) \to α_i)$$$

Lean4

/-- `AddMonoid.SMul` is measurable. -/
instance measurableSMul_nat₂ (M : Type*) [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] : MeasurableSMul₂ ℕ M :=
  ⟨by
    suffices Measurable fun p : M × ℕ => p.2 • p.1 by apply this.comp measurable_swap
    refine measurable_from_prod_countable_left fun n => ?_
    induction n with
    | zero => simp only [zero_smul, ← Pi.zero_def, measurable_zero]
    | succ n ih =>
      simp only [succ_nsmul]
      exact ih.add measurable_id⟩

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