isOrderedMonoid — Mathlib

English

Pull back an IsOrderedMonoid along an injective map; the order is preserved via the map.

Русский

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

LaTeX

$$$\\text{IsOrderedMonoid}(\\beta) \\leftarrow \\text{Injective isOrderedMonoid}$$$

Lean4

/-- Pullback an `IsOrderedMonoid` under an injective map. -/
@[to_additive /-- Pullback an `IsOrderedAddMonoid` under an injective map. -/
    ]
theorem isOrderedMonoid [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] (f : β → α)
    (mul : ∀ x y, f (x * y) = f x * f y) (le : ∀ {x y}, f x ≤ f y ↔ x ≤ y) : IsOrderedMonoid β where
  mul_le_mul_left a b ab c := le.1 <| by rw [mul, mul]; apply mul_le_mul_left'; exact le.2 ab

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