coe_dual — Mathlib

English

The dual of a nonempty interval corresponds to pulling back along the dual order; under the set-level identification, it is the preimage under OrderDual.ofDual.

Русский

Дуальная интервал соответствует отображению вдоль дуального порядка; на уровне множеств это предобраз OrderDual.ofDual.

LaTeX

$$$ \mathrm{coe}(\text{dual}\ s) = \mathrm{preimage}(\mathrm{ofDual}) (\mathrm{coe}(s)) $$$

Lean4

@[simp, norm_cast]
theorem coe_dual (s : NonemptyInterval α) : (dual s : Set αᵒᵈ) = ofDual ⁻¹' s :=
  Icc_toDual

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