measurableSet_toMeasurable — Mathlib

English

If s is a set, then toMeasurable μ s is measurable.

Русский

Для множества s оболочка toMeasurable μ s является измеримой.

LaTeX

$$MeasurableSet(toMeasurable(μ,s))$$

Lean4

@[simp]
theorem measurableSet_toMeasurable (μ : Measure α) (s : Set α) : MeasurableSet (toMeasurable μ s) :=
  by
  rw [toMeasurable_def]; split_ifs with hs h's
  exacts [hs.choose_spec.2.1, h's.choose_spec.2.1, (exists_measurable_superset μ s).choose_spec.2.1]

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