of — Mathlib · SciLib

English

For each i, there is a canonical monoid homomorphism of i: G_i → PushoutI φ, the i-th inclusion into the pushout.

Русский

Пусть для каждого i существует канонический моноид-гомоморфизм of_i: G_i → PushoutI φ — включение i-го компонента в пушаут.

LaTeX

$$$of_i : G_i \to^* PushoutI(\phi)$$$

Lean4

/-- The map from each indexing group into the pushout -/
def of (i : ι) : G i →* PushoutI φ :=
  (Con.mk' _).comp <| inl.comp CoprodI.of

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