Icc_toDual — Mathlib

English

For a locally finite order α, the closed interval between a and b in the dual order equals the image of the interval between b and a under the dual embedding.

Русский

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

LaTeX

$$$Icc(toDual a)(toDual b) = (Icc b a).map toDual.toEmbedding$$$

Lean4

theorem Icc_toDual : Icc (toDual a) (toDual b) = (Icc b a).map toDual.toEmbedding :=
  map_refl.symm

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