English
Pull back an IsOrderedMonoid via a strictly monotone map; the resulting β inherits the ordered monoid structure.
Русский
Переносим IsOrderedMonoid через строго монотонное отображение; β получает упорядоченный моноид.
LaTeX
$$$\\text{IsOrderedMonoid}(\\beta)$ via \\text{StrictMono}$$
Lean4
/-- Pullback an `IsOrderedCancelMonoid` under an injective map. -/
@[to_additive Function.Injective.isOrderedCancelAddMonoid /--
Pullback an `IsOrderedCancelAddMonoid` under an injective map. -/
]
theorem isOrderedCancelMonoid [IsOrderedCancelMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α)
(mul : ∀ x y, f (x * y) = f x * f y) (le : ∀ {x y}, f x ≤ f y ↔ x ≤ y) : IsOrderedCancelMonoid β
where
__ := Function.Injective.isOrderedMonoid f mul le
le_of_mul_le_mul_left a b c bc := le.1 <| (mul_le_mul_iff_left (f a)).1 (by rwa [← mul, ← mul, le])
