inclusion — Mathlib

English

The inclusion map corresponds to an inclusion of submonoids: every element of S maps into T, preserving the monoid operation.

Русский

Включение отображает включение подмножества: каждый элемент S переходит в T и сохраняет операцию моноида.

LaTeX

$$$ \text{Inclusion}(h) : S \to* T \quad \text{is a monoid hom}$$$

Lean4

/-- The monoid hom associated to an inclusion of submonoids. -/
@[to_additive /-- The `AddMonoid` hom associated to an inclusion of submonoids. -/
    ]
def inclusion {S T : Submonoid M} (h : S ≤ T) : S →* T :=
  S.subtype.codRestrict _ fun x => h x.2

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