support_restrict_subset — Mathlib

English

For any subset s, the support of the restricted measure μ|s is contained in the intersection of the closure of s with the original support μ.

Русский

Для любого множества s опора ограниченной меры μ|s лежит внутри пересечения замыкания s и опоры μ.

LaTeX

$$$ (\mu|_s).\operatorname{support} \subseteq \overline{s} \cap \operatorname{support}(\mu) $$$

Lean4

theorem support_restrict_subset {s : Set X} : (μ.restrict s).support ⊆ closure s ∩ μ.support :=
  by
  refine Set.subset_inter (support_subset_of_isClosed isClosed_closure ?_) (support_mono restrict_le_self)
  rw [mem_ae_iff, μ.restrict_apply isClosed_closure.isOpen_compl.measurableSet]
  convert μ.empty
  exact subset_closure.disjoint_compl_left.eq_bot

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