nhds_le_of_le — Mathlib

English

If s is an open neighborhood of x and 𝓟(s) ≤ f, then 𝓝 x ≤ f.

Русский

Если s открыто и содержит x, и 𝓟(s) ≤ f, то 𝓝 x ≤ f.

LaTeX

$$$x\\in s,\\; IsOpen(s),\\; 𝓟(s) \\le f \\Rightarrow 𝓝_x \\le f$$$

Lean4

/-- To show a filter is above the neighborhood filter at `x`, it suffices to show that it is above
the principal filter of some open set `s` containing `x`. -/
theorem nhds_le_of_le {f} (h : x ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 x ≤ f := by rw [nhds_def];
  exact iInf₂_le_of_le s ⟨h, o⟩ sf

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