map₂_def — Mathlib

English

The value of lift₂ on a pair is given by the universal construction, equating the result with ih i applied to the images under f₁ and f₂.

Русский

Значение lift₂ на пару задаётся универсальным построением, и равно ih i применённому к образам через f₁ и f₂.

LaTeX

$$$\\mathrm{lift\\_2\\_def}\\;(x,y,i,hxi,hyi) : \\mathrm{DirectLimit.lift\\_2}\\; f_1\\; f_2\\; ih\\; compat\\; ⟦x⟧ ⟦y⟧ = ih i (f_1 \\_ \\_ hxi x.2) (f_2 \\_ \\_ hyi y.2)$$$

Lean4

theorem map₂_def (i x y) : map₂ f₁ f₂ f ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ⟦⟨i, ih i x y⟩⟧ :=
  lift₂_def ..

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