orderMonoidHom_strictMono — Mathlib

English

The map orderMonoidHom G is strictly increasing; i.e., for all a<b, orderMonoidHom G (a) < orderMonoidHom G (b).

Русский

Отображение orderMonoidHom G строго возрастает: для любых a<b выполняется orderMonoidHom G(a) < orderMonoidHom G(b).

LaTeX

$$$\forall a,b\in G,\ a

Lean4

theorem orderMonoidHom_strictMono {G : Type*} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] : StrictMono (orderMonoidHom G) := let : LocallyFiniteOrder (Additive G) := ‹LocallyFiniteOrder G› fun a b h ↦ orderAddMonoidHom_strictMono h

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