English
If a filter f on X is dominated by nhds x for some x, then f ≤ nhds(lim f).
Русский
Если фильтр f на X ограничен сверху окном nhds x для некоторого x, то f ⊆ nhds(lim f).
LaTeX
$$$\exists x, f \le \nhds x \Rightarrow f \le \nhds(\lim f)$$$
Lean4
/-- If a filter `f` is majorated by some `𝓝 x`, then it is majorated by `𝓝 (Filter.lim f)`. We
formulate this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for
types without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify
this instance with any other instance. -/
theorem le_nhds_lim {f : Filter X} (h : ∃ x, f ≤ 𝓝 x) : f ≤ 𝓝 (@lim _ _ h.nonempty f) :=
Classical.epsilon_spec h
