uIcc_toDual — Mathlib

English

The upper-interval under the dual order corresponds to the image of the upper-interval under the dual embedding.

Русский

Удобный верхний интервал в двойственном порядке соответствует образу верхнего интервала через вложение двойственности.

LaTeX

$$"[[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding"$$

Lean4

theorem uIcc_toDual (a b : α) : [[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding :=
  Icc_toDual (a ⊔ b) (a ⊓ b)

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