isUpperSet_of_isOpen — Mathlib

English

A refined topological basis is formed by inserting the universal set into the subbasis of complements of Ici a.

Русский

Уточнённый топологический базис формируется добавлением всеобщего множества к подбазе комплиментов Ici a.

LaTeX

$$$\\text{IsTopologicalBasis}(\\operatorname{insert}(\\mathrm{univ}, \\{s: Set(\\alpha) \\mid \\exists a, (\\Ici a)^{c} = s\\}))$$$

Lean4

/-- Every set open in the upper topology is a upper set. -/
theorem isUpperSet_of_isOpen (h : IsOpen s) : IsUpperSet s :=
  IsLower.isLowerSet_of_isOpen (α := αᵒᵈ) h

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