English
In the WithZeroTopology construction, the neighborhood filter at 0 is the infimum over γ ≠ 0 of principal filters on the sets {y : γ > y}.
Русский
В конструкции WithZeroTopology фильтр окрестности нуля равен инфиминуму над γ ≠ 0 главными фильтрами на множествах {y : γ > y}.
LaTeX
$$$\mathcal{N}(0) = \bigwedge_{\gamma \ne 0} \mathcal{P}(Iio(\gamma))$$$
Lean4
theorem nhds_eq_update : (𝓝 : Γ₀ → Filter Γ₀) = update pure 0 (⨅ γ ≠ 0, 𝓟 (Iio γ)) :=
by
rw [nhds_nhdsAdjoint, sup_of_le_right]
exact le_iInf₂ fun γ hγ ↦ le_principal_iff.2 <| zero_lt_iff.2 hγ