nhdsWithin_eq — Mathlib

English

Neighborhood within a set equals infimum of principal filters intersected with the set.

Русский

Окрестность внутри множества равна инфимууму базовых фильтров, обрезанных пересечением с множеством.

LaTeX

$$$\text{nhdsWithin}(a,s) = \bigwedge_{t: Set} 𝓟(t \cap s)$$$

Lean4

theorem nhdsWithin_eq (a : α) (s : Set α) : 𝓝[s] a = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, 𝓟 (t ∩ s) :=
  ((nhds_basis_opens a).inf_principal s).eq_biInf

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