divRight — Mathlib

English

The map x ↦ x / a is an order isomorphism α ≃o α with the order reversed on the right.

Русский

Отображение x ↦ x / a является порядковым преобразованием α, сохраняющим обратный порядок на правой стороне.

LaTeX

$$OrderIso.divRight(a) : α ≃o α$$

Lean4

/-- `x ↦ x / a` as an order isomorphism. -/
@[to_additive (attr := simps!) /-- `x ↦ x - a` as an order isomorphism. -/
    ]
def divRight (a : α) : α ≃o α where
  toEquiv := Equiv.divRight a
  map_rel_iff' {_ _} := div_le_div_iff_right a

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