instIsLower — Mathlib

English

For a complete linear order α, the lower basis yields an explicit topological space basis description: open sets are either univ or the complement of Ici a, and this basis describes IsOpen equivalence.

Русский

Для полного линейного упорядочения α база нижней топологии описывает открытые множества как универ, или дополнения к Ici a, задавая эквивалентность IsOpen.

LaTeX

$$$\\text{IsOpen}(U) \\iff U = \\mathrm{univ} \\lor \\exists a, U = (\\Ici(a))^{c}$$$

Lean4

instance _root_.OrderDual.instIsLower [Preorder α] [TopologicalSpace α] [IsUpper α] : IsLower αᵒᵈ where
  topology_eq_lowerTopology := topology_eq_upperTopology (α := α)

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