mem_nhdsWithin_iff_eventuallyEq — Mathlib

English

For sets s,t and a point x, t is in 𝓝[s] x if and only if s is eventually equal to s ∩ t in the nhds at x.

Русский

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

LaTeX

$$$ t \in \mathcal{N}_s(x) \iff s =^{\mathcal{N}(x)} (s \cap t) $$$

Lean4

theorem mem_nhdsWithin_iff_eventuallyEq {s t : Set α} {x : α} : t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] (s ∩ t : Set α) := by
  simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]

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