isOpen_iff — Mathlib

English

A set of filters is open iff it can be expressed as a union of basic sets generated by Iic(𝓟 t).

Русский

Множество фильтров открыто тогда, когда его можно выразить как объединение базисных множеств Iic(𝓟 t).

LaTeX

$$$$\text{IsOpen } s \iff \exists T\subseteq \text{Set}(\alpha),\; s=\bigcup_{t\in T} Iic(\mathcal{P} t).$$$$

Lean4

theorem isOpen_iff {s : Set (Filter α)} : IsOpen s ↔ ∃ T : Set (Set α), s = ⋃ t ∈ T, Iic (𝓟 t) :=
  isTopologicalBasis_Iic_principal.open_iff_eq_sUnion.trans <| by
    simp only [exists_subset_range_and_iff, sUnion_image, (· ∘ ·)]

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