isOpen_setOf_mem — Mathlib

English

For any s, the set of filters containing s is open in the Filter topology.

Русский

Для любого s множество фильтров, содержащих s, открыто в топологическом пространстве Filter.

LaTeX

$$$$\{\ell\in\text{Filter }\alpha\;|\; s\in \ell\}\;\text{ is open in }\text{Filter}(\alpha).$$$$

Lean4

theorem isOpen_setOf_mem {s : Set α} : IsOpen {l : Filter α | s ∈ l} := by
  simpa only [Iic_principal] using isOpen_Iic_principal

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