Icc_ofDual — Mathlib

English

Let α be a locally finite preorder. For a,b in αᵒᵈ, the closed interval from a to b in the dual equals the image of the closed interval from b to a in α under the embedding.

Русский

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

LaTeX

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

Lean4

theorem Icc_ofDual (a b : αᵒᵈ) : Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding :=
  map_refl.symm

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