eventually_mem_nhds_iff — Mathlib

English

For any set s, (∀ᶠ x' in 𝓝 x, s ∈ 𝓝 x') holds if and only if s ∈ 𝓝 x.

Русский

Для любого множества s равносильно: (для большинства x' вокруг x) s ∈ 𝓝 x' тогда и только тогда s ∈ 𝓝 x.

LaTeX

$$$(\\forall^* x' \\in 𝓝 x,\\ s \\in 𝓝 x') \\;\\Leftrightarrow\\; s \\in 𝓝 x.$$$

Lean4

@[simp]
theorem eventually_mem_nhds_iff : (∀ᶠ x' in 𝓝 x, s ∈ 𝓝 x') ↔ s ∈ 𝓝 x :=
  eventually_eventually_nhds

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