volume_pos_of_nhds_real — Mathlib

English

If a predicate p holds eventually in a neighborhood of a real number a, then the volume of the set {x : p x} is strictly positive.

Русский

Если свойство p выполняется в окрестности точки a, то объем множества {x : p x} положителен.

LaTeX

$$$\forall {p : \mathbb{R} \to \mathsf{Prop}} {a : \mathbb{R}}, (\forallᶠ x \in nhds(a), p x) \Rightarrow 0 < \operatorname{volume}({x \mid p x})$$$

Lean4

theorem _root_.Filter.Eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ x in 𝓝 a, p x) :
    (0 : ℝ≥0∞) < volume {x | p x} :=
  by
  rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩
  grw [← hs]
  simpa [-mem_Ioo] using hx.1.trans hx.2

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