eventually_eventually_nhdsWithin — Mathlib

English

Equivalence expressing nhdsWithin as an infimum of principal filters over opens around a.

Русский

Эквивалентность nhdsWithin как инфимума базовых фильтров над открытыми окрестностями a.

LaTeX

$$$𝓝[s] a = \bigsqcup_{t\ni a\in t \land IsOpen t} 𝓟(t \cap s)$$$

Lean4

@[simp]
theorem eventually_eventually_nhdsWithin {a : α} {s : Set α} {p : α → Prop} :
    (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x :=
  by
  refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
  simp only [eventually_nhdsWithin_iff] at h ⊢
  exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

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