mk — Mathlib · SciLib

English

Constructor for the composition of multivariate functors, assembling the A and B components from P and Q.

Русский

Конструктор композиции мультфункторов, собирающий A и B компоненты из P и Q.

LaTeX

$$$$ \\mathrm{comp}.mk(x) = \\langle \\langle x.1.1, \\dots \\rangle, \\dots \\rangle. $$$$

Lean4

/-- Constructor for functor composition -/
def mk (x : P (fun i => Q i α)) : comp P Q α :=
  ⟨⟨x.1, fun _ a => (x.2 _ a).1⟩, fun i a => (x.snd a.fst a.snd.fst).snd i a.snd.snd⟩

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