strictMono_subsemigroupCongr — Mathlib

English

If two subsemigroups S and T are equal, the induced congruence map is strictly monotone.

Русский

Если два подпполугруппы S и T равны, то индуцированное отображение конгруэнтности строго монотонно.

LaTeX

$$StrictMono( subsemigroupCongr h )$$

Lean4

@[to_additive]
theorem strictMono_subsemigroupCongr {G : Type*} [CommMonoid G] [PartialOrder G] {S T : Subsemigroup G} (h : S = T) :
    StrictMono (subsemigroupCongr h) := fun _ _ ↦ id

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