instTopologicalSpace — Mathlib

English

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

Русский

Наблюдательный фильтр окрестности l равен подъёму главного фильтра по Iic ∘ 𝓟.

LaTeX

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

Lean4

/-- The topology on `Filter α` is generated by the sets `Set.Iic (𝓟 s) = {l : Filter α | s ∈ l}`,
`s : Set α`. A set `s : Set (Filter α)` is open if and only if it is a union of a family of these
basic open sets, see `Filter.isOpen_iff`. -/
instance : TopologicalSpace (Filter α) :=
  generateFrom <| range <| Iic ∘ 𝓟

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