instOrderIsoClass — Mathlib

English

The type of order isomorphisms α ≃o β forms an OrderIsoClass, i.e., maps preserve and reflect order.

Русский

Тип отображений тождественных по порядку α ≃o β образует класс OrderIso, сохраняющий и отражающий порядок.

LaTeX

$$$\text{OrderIsoClass}(\alpha \simeq_o \beta, \alpha, \beta)$$$

Lean4

instance : OrderIsoClass (α ≃o β) α β where map_le_map_iff f _ _ := f.map_rel_iff'

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