exists_mem_forall_mem_nhdsWithin_pos_measure

English

If μ(s) ≠ 0, there exists x ∈ s such that for every t ∈ 𝓝[s] x we have μ(t) > 0.

Русский

Если μ(s) ≠ 0, существует точка x ∈ s такая, что для любой окрестности t внутри s с x, μ(t) > 0.

LaTeX

$$$\\\\exists x\\\\in s, \\\\forall t \\\\in 𝓝[s] x, \\\\ 0 < μ(t)$$$

Lean4

/-- If `m s ≠ 0`, then for some point `x ∈ s` and any `t ∈ 𝓝[s] x` we have `0 < m t`. -/
theorem exists_mem_forall_mem_nhdsWithin_pos_measure [TopologicalSpace α] [SecondCountableTopology α] {s : Set α}
    (hs : μ s ≠ 0) : ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < μ t :=
  by
  contrapose! hs
  simp only [nonpos_iff_eq_zero] at hs
  exact measure_null_of_locally_null s hs

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