measurableZPow — Mathlib

English

For any DivInvMonoid G with measurable structure, the map (g,n) ↦ g^n is measurable where n ∈ ℤ.

Русский

Пусть G — DivInvMonoid с измеримой структурой; отображение (g,n) ↦ g^n (n ∈ ℤ) измеримо.

LaTeX

$$$\\text{MeasurablePow}\ G\\ \\mathbb{Z}$$$

Lean4

/-- `DivInvMonoid.Pow` is measurable. -/
instance measurableZPow (G : Type u) [DivInvMonoid G] [MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G] :
    MeasurablePow G ℤ :=
  ⟨measurable_from_prod_countable_left fun n => by
      rcases n with n | n
      · simp_rw [Int.ofNat_eq_coe, zpow_natCast]
        exact measurable_id.pow_const _
      · simp_rw [zpow_negSucc]
        exact (measurable_id.pow_const (n + 1)).inv⟩

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