instOrderTopologyOrderDual — Mathlib

English

If α has an order topology, then the dual order αᵒᵈ also carries an order topology; it is obtained by swapping the roles of the two half-line subbase intervals.

Русский

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

LaTeX

$$$\\text{OrderTopology}(\\alpha^{\\mathrm{op}}) \\text{ существует и определяется аналогично через обмен интервалов}$$$

Lean4

instance [t : OrderTopology α] : OrderTopology αᵒᵈ :=
  ⟨by
    convert OrderTopology.topology_eq_generate_intervals (α := α) using 6
    apply or_comm⟩

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