divLeft — Mathlib

English

The map x ↦ a / x is an order-reversing equivalence α ≃o αᵒᵈ when α is a group with suitable order structure.

Русский

Отображение x ↦ a / x является порядковым обратным эквивалентом α ≃o αᵒᵈ при группе с нужной структурой порядка.

LaTeX

$$OrderIso.divLeft(a) : α ≃o α^{\mathrm{op}}$$

Lean4

/-- `x ↦ a / x` as an order-reversing equivalence. -/
@[to_additive (attr := simps!) /-- `x ↦ a - x` as an order-reversing equivalence. -/
    ]
def divLeft (a : α) : α ≃o αᵒᵈ where
  toEquiv := (Equiv.divLeft a).trans OrderDual.toDual
  map_rel_iff' {_ _} := div_le_div_iff_left (α := α) _

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