English
If s is everywhere positive for μ and ν coincides with μ locally around every x ∈ s (i.e., for each x ∈ s there is a neighborhood t of x with ν(u) = μ(u) for all u ⊆ t), then ν is everywhere positive on s.
Русский
Если s является повсюду положительным по мере μ, и μ и ν совпадают локально вокруг каждой точки x ∈ s (то есть существует окрестность t x, такая что для любых подмножеств u ⊆ t, ν(u) = μ(u)), то ν является повсюду положительной на s.
LaTeX
$$IsEverywherePos(μ, s) → (∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u) → IsEverywherePos(ν, s)$$
Lean4
/-- If two measures coincide locally, then a set which is everywhere positive for the former is
also everywhere positive for the latter. -/
theorem of_forall_exists_nhds_eq (hs : IsEverywherePos μ s) (h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u) :
IsEverywherePos ν s := by
intro x hx n hn
rcases h x hx with ⟨t, t_mem, ht⟩
grw [← inter_subset_left (s := n)]
rw [ht (n ∩ t) inter_subset_right]
exact hs x hx _ (inter_mem hn (mem_nhdsWithin_of_mem_nhds t_mem))
