measurableInv — Mathlib

English

If each coordinate has an inverse that is measurable, then the inversion on the product space ∀ i, α_i is measurable.

Русский

Если для каждого координатного пространства выполняется измеримость обратной операции, то обращение на произведении координат измеримо.

LaTeX

$$$\\text{MeasurableInv}((i\\mapsto α_i))$$$

Lean4

@[to_additive]
instance measurableInv {ι : Type*} {α : ι → Type*} [∀ i, Inv (α i)] [∀ i, MeasurableSpace (α i)]
    [∀ i, MeasurableInv (α i)] : MeasurableInv (∀ i, α i) :=
  ⟨measurable_pi_iff.mpr fun i => (measurable_pi_apply i).inv⟩

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