measurable_mem — Mathlib

English

For a fixed subset s ⊆ α, the map x ↦ (x ∈ s) is measurable if and only if s is measurable.

Русский

Для фиксированного множества s ⊆ α отображение x ↦ (x ∈ s) измеримо тогда и только тогда, когда s измеримо.

LaTeX

$$$\mathrm{Measurable}(x \mapsto x \in s) \iff \mathrm{MeasurableSet}(s)$$$

Lean4

@[simp]
theorem measurable_mem : Measurable (· ∈ s) ↔ MeasurableSet s :=
  measurableSet_setOf.symm

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