instIsUpperSet — Mathlib

English

If α has a lower-set topology, then the order dual αᵒᵈ carries an upper-set topology.

Русский

Если у α есть топология нижних множеств, то у порядка двойника αᵒᵈ возникает топология верхних множеств.

LaTeX

$$$$ \\text{If } \\text{LowerSet}(\\alpha) \\text{ holds, then } \\text{UpperSet}(\\alpha^{\\mathrm{op}}). $$$$

Lean4

instance _root_.OrderDual.instIsUpperSet [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] :
    Topology.IsUpperSet αᵒᵈ where topology_eq_upperSetTopology := by ext; rw [IsLowerSet.topology_eq α]

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