mem_nhdsWithin_iff_eventually — Mathlib

English

For sets s,t and a point x, membership of t in the restricted neighborhood 𝓝[s] x is equivalent to检 the eventual membership of y in nhds x implying y ∈ s → y ∈ t.

Русский

Для множеств s,t и точки x принадлежность t окрестности 𝓝[s] x эквивалентна условию, что почти во всех y в 𝓝 x, из y ∈ s следует y ∈ t.

LaTeX

$$$ t \in \mathcal{N}_s(x) \iff \forall^{\infty} y \in \mathcal{N}(x),\ y \in s \rightarrow y \in t $$$

Lean4

theorem mem_nhdsWithin_iff_eventually {s t : Set α} {x : α} : t ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t :=
  eventually_inf_principal

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