English
Let μ be a measure on a topological space X and s ⊆ X. Then every point in int(s) that lies in the support of μ also lies in the support of the restricted measure μ|s.
Русский
Пусть μ — мера на топологическом пространстве X и s ⊆ X. Тогда любая точка из int(s), лежащая в опоре μ, также лежит в опоре ограниченной меры μ|s.
LaTeX
$$$ \operatorname{int}(s) \cap \operatorname{supp}(\mu) \subseteq \operatorname{supp}(\mu|_s) $$$
Lean4
theorem interior_inter_support {s : Set X} : interior s ∩ μ.support ⊆ (μ.restrict s).support :=
by
rintro x ⟨hxs, hxμ⟩
rw [mem_support_restrict, (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]
rw [(nhds_basis_opens x).mem_measureSupport] at hxμ
rintro u ⟨hxu, hu⟩
apply hxμ (u ∩ interior s) ⟨⟨hxu, hxs⟩, hu.inter isOpen_interior⟩ |>.trans_le
gcongr
exact interior_subset
