Ico_orderDual_def — Mathlib

English

For a locally finite order α, the closed interval Icc(a,b) in α is in bijection with the image of Icc(b,a) under the order dual embedding.

Русский

Для локально конечного порядка α замкнутый интервал Icc(a,b) в α биективно связан с образом Icc(b,a) через отображение двойственного порядка.

LaTeX

$$$\mathrm{Icc}(a,b) = \mathrm{map} \big(\mathrm{toDual.toEmbedding}\big)\big( \mathrm{Icc}(b,a) \big)$$$

Lean4

theorem Ico_orderDual_def (a b : αᵒᵈ) : Ico a b = (Ioc (ofDual b) (ofDual a)).map toDual.toEmbedding :=
  map_refl.symm

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