dual — Mathlib

English

There exists an equivalence between NonemptyInterval α and NonemptyInterval αᵒᵈ given by swapping endpoints.

Русский

Существует эквивалентность между NonemptyInterval α и NonemptyInterval αᵒᵈ, задаваемая обменом концов интервалов.

LaTeX

$$$\mathrm{dual} : \mathrm{NonemptyInterval}\;\alpha \simeq \mathrm{NonemptyInterval}\;\alpha^{\mathrm{OrderDual}}$$$

Lean4

/-- Turn an interval into an interval in the dual order. -/
def dual : NonemptyInterval α ≃ NonemptyInterval αᵒᵈ
    where
  toFun s := ⟨s.toProd.swap, s.fst_le_snd⟩
  invFun s := ⟨s.toProd.swap, s.fst_le_snd⟩

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