isEverywherePos_iff_of_forall_exists_nhds_eq

English

If two measures ν and μ agree locally on s in the sense that for every x ∈ s there exists a neighborhood t of x with ν u = μ u for all subsets u ⊆ t, then IsEverywherePos ν s holds iff IsEverywherePos μ s holds.

Русский

Если две меры ν и μ совпадают локально на s так, что для каждой точки x ∈ s существует окрестность t такой, что для любых подмножеств u ⊆ t выполняется ν u = μ u, тогда μIsEverywherePos s и νIsEverywherePos s эквивалентны.

LaTeX

$$IsEverywherePos(ν, s) ↔ IsEverywherePos(μ, s)$$

Lean4

/-- If two measures coincide locally, then a set is everywhere positive for the former iff it is
everywhere positive for the latter. -/
theorem isEverywherePos_iff_of_forall_exists_nhds_eq (h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u) :
    IsEverywherePos ν s ↔ IsEverywherePos μ s :=
  by
  refine ⟨fun H ↦ H.of_forall_exists_nhds_eq ?_, fun H ↦ H.of_forall_exists_nhds_eq h⟩
  intro x hx
  rcases h x hx with ⟨t, ht, h't⟩
  exact ⟨t, ht, fun u hu ↦ (h't u hu).symm⟩

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