self_mem_ae_restrict — Mathlib

English

For measurable set s, s itself is a member of ae μ|_s (simplified).

Русский

Для измеримого s, множество s принадлежит ae μ|_s (упрощенно).

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow s \in \ae(μ|_s).$$$

Lean4

theorem self_mem_ae_restrict {s} (hs : MeasurableSet s) : s ∈ ae (μ.restrict s) :=
  by
  simp only [ae_restrict_eq hs, mem_principal, mem_inf_iff]
  exact ⟨_, univ_mem, s, Subset.rfl, (univ_inter s).symm⟩

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