subset_toMeasurable — Mathlib

English

Every set s is contained in its measurable hull toMeasurable μ s.

Русский

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

LaTeX

$$s ⊆ toMeasurable(μ,s)$$

Lean4

theorem subset_toMeasurable (μ : Measure α) (s : Set α) : s ⊆ toMeasurable μ s :=
  by
  rw [toMeasurable_def]; split_ifs with hs h's
  exacts [hs.choose_spec.1, h's.choose_spec.1, (exists_measurable_superset μ s).choose_spec.1]

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