nhdsWithin_eq_iff_eventuallyEq — Mathlib

English

Equality of restricted neighborhoods: 𝓝[s] x equals 𝓝[t] x if and only if s and t coincide up to nhds x on x.

Русский

Равенство окрестностей внутри: 𝓝[s] x равно 𝓝[t] x тогда, когда s и t совпадают по окрестности x.

LaTeX

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

Lean4

theorem nhdsWithin_eq_iff_eventuallyEq {s t : Set α} {x : α} : 𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t :=
  set_eventuallyEq_iff_inf_principal.symm

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