inclusion — Mathlib

English

The semigroup hom arising from an inclusion h: S ≤ T between subsemigroups S ⊆ T is the map that sends each element of S to itself viewed as an element of T.

Русский

Полугомом, полученный из включения h: S ≤ T между подполугруппами S ⊆ T, является отображение, отправляющее каждый элемент S на сам элемент S, рассматриваемый как элемент T.

LaTeX

$$$\text{inclusion}_{S,T}(x) = x$ for all x ∈ S$$$

Lean4

/-- The semigroup hom associated to an inclusion of subsemigroups. -/
@[to_additive /-- The `AddSemigroup` hom associated to an inclusion of subsemigroups. -/
    ]
def inclusion {S T : Subsemigroup M} (h : S ≤ T) : S →ₙ* T :=
  (MulMemClass.subtype S).codRestrict _ fun x => h x.2

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