isEverywherePos — Mathlib

English

If a measure μ is positive on open sets and s is open, then s is everywhere positive with respect to μ.

Русский

Если мера μ положительна на открытых множествах и множество s открыто, то s является повсюду положительным по μ.

LaTeX

$$[IsOpenPosMeasure μ] IsOpen s → IsEverywherePos μ s$$

Lean4

/-- An open set is everywhere positive for a measure which is positive on open sets. -/
theorem _root_.IsOpen.isEverywherePos [IsOpenPosMeasure μ] (hs : IsOpen s) : IsEverywherePos μ s :=
  by
  intro x xs n hn
  rcases mem_nhdsWithin.1 hn with ⟨u, u_open, xu, hu⟩
  apply lt_of_lt_of_le _ (measure_mono hu)
  exact (u_open.inter hs).measure_pos μ ⟨x, ⟨xu, xs⟩⟩

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