measurableSet_swap_iff — Mathlib

English

The preimage of a set under the swap map is measurable exactly when the set is measurable: MeasurableSet (Prod.swap⁻¹' s) ↔ MeasurableSet s.

Русский

Пусть s — множество в парном пространстве. Обратное изображение под обменом координат измеримо тогда и только тогда, когда само множество измеримо: MeasurableSet (Prod.swap⁻¹' s) ↔ MeasurableSet s.

LaTeX

$$$\operatorname{MeasurableSet}(\mathrm{Prod.swap}^{-1}' s) \iff \operatorname{MeasurableSet} s$$$

Lean4

theorem measurableSet_swap_iff {s : Set (α × β)} : MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s :=
  ⟨fun hs => measurable_swap hs, fun hs => measurable_swap hs⟩

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