isOrderedMonoid — Mathlib

English

Pull back an IsOrderedCancelMonoid along an injective map; the ordering and cancellation properties are preserved.

Русский

Переносим IsOrderedCancelMonoid вдоль инъективного отображения; сохраняются порядок и отменяемость.

LaTeX

$$$\\text{IsOrderedCancelMonoid}(\\beta)$$$

Lean4

/-- Pullback an `IsOrderedMonoid` under a strictly monotone map. -/
@[to_additive /-- Pullback an `IsOrderedAddMonoid` under a strictly monotone map. -/
    ]
theorem isOrderedMonoid [IsOrderedMonoid α] [CommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f)
    (mul : ∀ x y, f (x * y) = f x * f y) : IsOrderedMonoid β :=
  Function.Injective.isOrderedMonoid f mul hf.le_iff_le

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