of — Mathlib · SciLib

English

There is a canonical embedding G → HNNExtension G A B φ, given by the map that includes G into the HNN extension.

Русский

Существует каноническое вложение G в HNNExtension G A B φ, задаваемое отображением включения.

LaTeX

$$$ \\text{of} : G \\to HNNExtension G A B φ $$$

Lean4

/-- The canonical embedding `G →* HNNExtension G A B φ` -/
def of : G →* HNNExtension G A B φ :=
  (HNNExtension.con G A B φ).mk'.comp inl

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