isLowerSet_orderDual — Mathlib

English

The lower-set property for αᵒᵈ is equivalent to the upper-set property for α.

Русский

Свойство нижних множеств для αᵒᵈ эквивалентно свойству верхних множеств для α.

LaTeX

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

Lean4

theorem isLowerSet_orderDual [Preorder α] [TopologicalSpace α] : Topology.IsLowerSet αᵒᵈ ↔ Topology.IsUpperSet α :=
  isUpperSet_orderDual.symm

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