nhds_eq — Mathlib

English

The neighborhood filter at l is the lift of the principal filter along Iic ∘ 𝓟.

Русский

Фильтр окрестностей l — подъём главного фильтра по Iic ∘ 𝓟.

LaTeX

$$$$\mathcal{N}(l)=l.lift'(Iic\circ 𝓟).$$$$

Lean4

theorem nhds_eq (l : Filter α) : 𝓝 l = l.lift' (Iic ∘ 𝓟) :=
  nhds_generateFrom.trans <| by
    simp only [mem_setOf_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift, (· ∘ ·), mem_Iic,
      le_principal_iff]

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