measurableSet_image — 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'' s) \leftrightarrow MeasurableSet s $$$

Lean4

@[simp]
theorem measurableSet_image (e : α ≃ᵐ β) : MeasurableSet (e '' s) ↔ MeasurableSet s := by
  rw [image_eq_preimage, measurableSet_preimage]

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