toIsOrderedMonoid — Mathlib

English

A submonoid S of a commutative monoid M with a partial order that is ordered inherits IsOrderedMonoid.

Русский

Подмножество подмножество S под упорядоченным моноидом M наследует IsOrderedMonoid.

LaTeX

$$IsOrderedMonoid S$$

Lean4

/-- A submonoid of an ordered monoid is an ordered monoid. -/
@[to_additive /-- An `AddSubmonoid` of an ordered additive monoid is an ordered additive monoid. -/
    ]
instance (priority := 75) toIsOrderedMonoid [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] [SubmonoidClass S M]
    (s : S) : IsOrderedMonoid s :=
  Function.Injective.isOrderedMonoid Subtype.val (fun _ _ => rfl) .rfl

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