Ico_toDual — Mathlib

English

Let α be a preorder. For any a,b ∈ α, the half-open interval [toDual a, toDual b) in the dual order equals the preimage under the duality map of the half-open interval (b, a] in the original order.

Русский

Пусть α — предпорядок. Для любых a, b ∈ α полустроковый интервал [toDual a, toDual b) во втором порядке равен прообразу полузакрытого интервала (b, a] в исходном порядке под двойственным отображением.

LaTeX

$$$$ \\mathrm{Ico}(\\mathrm{toDual}(a), \\mathrm{toDual}(b)) = \\mathrm{ofDual}^{-1}\\'\\'\\mathrm{Ioc}(b, a). $$$$

Lean4

@[simp]
theorem Ico_toDual : Ico (toDual a) (toDual b) = ofDual ⁻¹' Ioc b a :=
  Set.ext fun _ => and_comm

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