uIcc_toDual — Mathlib

English

In the dual order, the unordered interval corresponds to the preimage of the original interval under the duality map.

Русский

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

LaTeX

$$$$ [[toDual\ a, toDual\ b]] = toDual^{-1}([[a,b]]). $$$$

Lean4

@[simp]
theorem uIcc_toDual (a b : α) : [[toDual a, toDual b]] = ofDual ⁻¹' [[a, b]] :=
  -- Note: needed to hint `(α := α)` after https://github.com/leanprover-community/mathlib4/pull/8386 (elaboration order?)

  Icc_toDual (α := α)

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