multiforkLift_map — Mathlib

English

For every i0, the map multiforkLift c composed with F.map (E.f i0)^{op} equals the i0-th leg of the multifork: multiforkLift c ≫ F.val.map (E.f i0).op = c.ι i0.

Русский

Для каждого i0 композиция multiforkLift c с F.map (E.f i0)^{op} равна i0-й ноге мультифорка: multiforkLift c ≫ F.val.map (E.f i0).op = c.ι i0.

LaTeX

$$$\mathrm{multiforkLift}(c) \; ≫\; F.\mathrm{val}.map (E.f i_0).op = c.ι i_0$$$

Lean4

@[reassoc]
theorem multiforkLift_map (i₀ : E.I₀) : multiforkLift c ≫ F.val.map (E.f i₀).op = c.ι i₀ := by simp [multiforkLift]

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