mk — Mathlib · SciLib

English

There is a constructor for forming the composition: given x ∈ F( i ↦ G i α ), the term Comp.mk x inhabits the composite object Comp F G α.

Русский

Существует конструктор образования композиции: дано x ∈ F( i ↦ G i α ), элемент Comp.mk x принадлежит композитному функтору Comp F G α.

LaTeX

$$$\operatorname{Comp.mk}(x) \in \operatorname{Comp} F G \alpha \quad\text{for}\quad x \in F\bigl(i \mapsto G i \alpha\bigr).$$$

Lean4

/-- Constructor for functor composition -/
protected def mk (x : F fun i ↦ G i α) : Comp F G α :=
  x

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