isTopologicalSpace_basis — Mathlib

English

If α is a complete linear order with a topology and IsUpper, the openness of a set U is equivalent to U being the whole space or U = (Iic a)^c for some a.

Русский

Пусть α —CompleteLinearOrder с топологией и IsUpper. Открытость множества U эквивалентна тому, что U есть вся пространство или U = (Iic a)^c для некоторого a.

LaTeX

$$$\forall U:\; IsOpen(U) \iff U = \mathrm{univ} \lor \exists a, (Iic\,a)^c = U$$$

Lean4

theorem isTopologicalSpace_basis (U : Set α) : IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U :=
  IsLower.isTopologicalSpace_basis (α := αᵒᵈ) U

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