measurableEmbedding_inv — Mathlib

English

The inversion map is a measurable embedding: it is injective, measurable, and its image preserves measurability of sets.

Русский

Обращение является измеримым вложением: оно инъективно, измеримо, и образ измеримых множеств сохраняется.

LaTeX

$$$\\text{MeasurableEmbedding}(\\mathrm{Inv}^{-1})$$$

Lean4

@[to_additive]
theorem measurableEmbedding_inv [InvolutiveInv α] [MeasurableInv α] : MeasurableEmbedding (Inv.inv (α := α)) :=
  ⟨inv_injective, measurable_inv, fun s hs ↦ s.image_inv_eq_inv ▸ hs.inv⟩

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