measurableSet_setOf — Mathlib

English

For predicate p on α, MeasurableSet {a ∈ α : p(a)} if and only if p is a measurable predicate.

Русский

Для предиката p на α множество {a ∈ α : p(a)} измеримо тогда и только тогда, когда p — измеримый предикат.

LaTeX

$$$\mathrm{MeasurableSet}\bigl\{a \in \alpha \mid p(a)\bigr\} \iff \mathrm{Measurable}(p)$$$

Lean4

@[simp]
theorem measurableSet_setOf : MeasurableSet {a | p a} ↔ Measurable p :=
  ⟨fun h ↦ measurable_to_prop <| by simpa only [preimage_singleton_true], fun h => by
    simpa using h (measurableSet_singleton True)⟩

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