toIsOrderedMonoid — Mathlib

English

A subgroup of an ordered group inherits an ordered monoid structure; that is, the subgroup with the inherited order is an ordered monoid.

Русский

Подгруппа упорядоченной группы наследует структуру упорядоченного моноида: подгруппа с унаследованным порядком является упорядоченным моноидом.

LaTeX

$$IsOrderedMonoid(H)$$

Lean4

/-- A subgroup of an ordered group is an ordered group. -/
@[to_additive /-- An `AddSubgroup` of an `AddOrderedCommGroup` is an `AddOrderedCommGroup`. -/
    ]
instance toIsOrderedMonoid [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] (H : Subgroup G) : IsOrderedMonoid H :=
  Function.Injective.isOrderedMonoid Subtype.val (fun _ _ => rfl) .rfl

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