isUpperSet_orderDual — Mathlib

English

The upper-set property of the order dual is equivalent to the lower-set property of the original order.

Русский

Свойство верхнего множества для порядка через двойник эквивалентно свойству нижнего множества для исходного порядка.

LaTeX

$$$$ \\text{IsUpperSet}(\\mathrm{OrderDual}(\\alpha)) \\;\\Longleftrightarrow\\; \\text{IsLowerSet}(\\alpha). $$$$

Lean4

theorem isUpperSet_orderDual [Preorder α] [TopologicalSpace α] : Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α :=
  by
  constructor
  · apply OrderDual.instIsLowerSet
  · apply OrderDual.instIsUpperSet

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