dual — Mathlib

English

There is a natural equivalence between intervals in α and intervals in α with the dual order.

Русский

Существует естественное эквивалентное соответствие между интервалами в α и интервалами в α в обратном порядке.

LaTeX

$$$ \mathrm{dual} : \mathrm{Interval}(\alpha) \simeq \mathrm{Interval}(\alpha^{\mathrm{op}}) $$$

Lean4

/-- Turn an interval into an interval in the dual order. -/
def dual : Interval α ≃ Interval αᵒᵈ :=
  NonemptyInterval.dual.withBotCongr

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