toOrderHomClassOrderDual — Mathlib

English

If F is a class of maps that preserves order between α and β, then the same class naturally extends to dual orders αᵒᵈ and βᵒᵈ with the same map_rel property.

Русский

Если F — класс отображений, сохраняющих порядок между α и β, то тот же класс естественным образом переносится на двойственные порядки αᵒᵈ и βᵒᵈ с тем же свойством map_rel.

LaTeX

$$$\\text{OrderHomClass } F \\ α^{\\mathrm{op}} \\ β^{\\mathrm{op}} \\text{ with } \\mathrm{map\\_rel} f := \\mathrm{map\\_rel} f.$$$

Lean4

instance (priority := 90) toOrderHomClassOrderDual [LE α] [LE β] [FunLike F α β] [OrderHomClass F α β] :
    OrderHomClass F αᵒᵈ βᵒᵈ where map_rel f := map_rel f

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