measurableSet_insert — Mathlib

English

For any a ∈ α and any s ⊆ α, MeasurableSet (insert a s) iff MeasurableSet s.

Русский

Для любого a и s: MeasurableSet (insert a s) тогда и только тогда, когда MeasurableSet s.

LaTeX

$$$\mathrm{MeasurableSet}(\mathrm{insert}\ a\ s) \leftrightarrow \mathrm{MeasurableSet}(s)$$$

Lean4

@[simp]
theorem measurableSet_insert {a : α} {s : Set α} : MeasurableSet (insert a s) ↔ MeasurableSet s := by
  classical
    exact
    ⟨fun h =>
      if ha : a ∈ s then by rwa [← insert_eq_of_mem ha] else insert_diff_self_of_notMem ha ▸ h.diff (.singleton _),
      fun h => h.insert a⟩

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