coe_dual — Mathlib

English

Under the dual order, the set of a dual interval equals the preimage of the original interval under the duality map.

Русский

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

LaTeX

$$$$ (dual\, s : Set \\alpha^{op}) = ofDual^{-1}' s. $$$$

Lean4

@[simp, norm_cast]
theorem coe_dual (s : Interval α) : (dual s : Set αᵒᵈ) = ofDual ⁻¹' s := by
  cases s with
  | bot => rfl
  | coe s₀ => exact NonemptyInterval.coe_dual s₀

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