nhds_eq_update — Mathlib

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γ

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