negOrderIso — Mathlib

English

The negation operation on EReal provides an order-reversing bijection between EReal and its order dual; x maps to -x.

Русский

Отрицание на EReal задаёт антиизоморфизм порядка между EReal и его двойственным порядком; отображение x ↦ −x.

LaTeX

$$$$EReal \cong_o EReal^{op},\ x \mapsto -x.$$$$

Lean4

/-- Negation as an order reversing isomorphism on `EReal`. -/
def negOrderIso : EReal ≃o ERealᵒᵈ :=
  { Equiv.neg EReal with
    toFun := fun x => OrderDual.toDual (-x)
    invFun := fun x => -OrderDual.ofDual x
    map_rel_iff' := neg_le_neg_iff }

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