isTopologicalBasis_insert_univ_subbasis

English

The collection formed by inserting the universal set into sets of the form (Iic a)ᶜ constitutes a topological basis for the upper topology.

Русский

Набор, полученный вставкой единицы (univ) в множества вида (Iic a)ᶜ, образует базу верхней топологии.

LaTeX

$$$\text{IsTopologicalBasis}(\text{insert univ }\{s: A\;|\;\exists a, (Iic\,a)^c = s\})$$$

Lean4

theorem isTopologicalBasis_insert_univ_subbasis : IsTopologicalBasis (insert univ {s : Set α | ∃ a, (Iic a)ᶜ = s}) :=
  IsLower.isTopologicalBasis_insert_univ_subbasis (α := αᵒᵈ)

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