measurablePow — Mathlib

English

In a measurable monoid M with a measurable multiplication, for every n ∈ ℕ the map a ↦ a^n is measurable.

Русский

В измеримом мономе M с измеримым умножением для каждого натурального n ∈ ℕ отображение a ↦ a^n измеримо.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\text{Measurable}(a \\mapsto a^n).$$$

Lean4

/-- `Monoid.Pow` is measurable. -/
instance measurablePow (M : Type*) [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] : MeasurablePow M ℕ :=
  ⟨measurable_from_prod_countable_left fun n => by
      induction n with
      | zero => simp only [pow_zero, ← Pi.one_def, measurable_one]
      | succ n ih =>
        simp only [pow_succ]
        exact ih.mul measurable_id⟩

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