measurableSet_preimage — Mathlib

English

For a measurable equivalence e and any set s in β, MeasurableSet (e⁻¹' s) is equivalent to MeasurableSet s.

Русский

Для измеримой эквивалентности e и любого множества s в β свойство измеримости предобраза e⁻¹'(s) эквивалентно измеримости s.

LaTeX

$$$ MeasurableSet (e^{-1}' s) \leftrightarrow MeasurableSet s $$$

Lean4

@[simp]
theorem measurableSet_preimage (e : α ≃ᵐ β) {s : Set β} : MeasurableSet (e ⁻¹' s) ↔ MeasurableSet s :=
  ⟨fun h => by simpa only [symm_preimage_preimage] using e.symm.measurable h, fun h => e.measurable h⟩

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