instNoAtoms — Mathlib

English

The restriction of a NoAtoms measure to any set also has no atoms.

Русский

Ограничение меры без атомов к любому множеству также не имеет атомов.

LaTeX

$$$$\text{Restriction of NoAtoms measure to }s\text{ is NoAtoms.}$$$$

Lean4

instance instNoAtoms (s : Set α) : NoAtoms (μ.restrict s) :=
  by
  refine ⟨fun x => ?_⟩
  obtain ⟨t, hxt, ht1, ht2⟩ := exists_measurable_superset_of_null (measure_singleton x : μ { x } = 0)
  apply measure_mono_null hxt
  rw [Measure.restrict_apply ht1]
  apply measure_mono_null inter_subset_left ht2

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