instIsLowerSet — Mathlib

English

The dual order αᵒᵈ inherits a lower-set structure from the IsUpperSet structure on α; i.e., αᵒᵈ is a LowerSet space.

Русский

Двойственный порядок αᵒᵈ наследует структуру нижнего множества от IsUpperSet на α; то есть αᵒᵈ — пространство нижних множеств.

LaTeX

$$$ \operatorname{IsLowerSet} (\alpha^{\mathrm{op}}).$$$

Lean4

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

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