toOrderIsoClassOrderDual — Mathlib

English

The dual of the domain and codomain preserves the order-iso class structure: if F is an order-iso class, then it remains an order-iso class between dual types.

Русский

Дуал порядка сохраняет структуру класса порядкового изоморфизма: если F образует класс порядковых изоморфизмов между α и β, то он сохраняется между их двойниками.

LaTeX

$$$ \text{OrderIsoClass } F\ (\alpha^{\mathrm{op}})\ (\beta^{\mathrm{op}}) $$$

Lean4

instance (priority := 90) toOrderIsoClassOrderDual [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] :
    OrderIsoClass F αᵒᵈ βᵒᵈ where map_le_map_iff f := map_le_map_iff f

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