inl_i — Mathlib

English

Let A be an object in a category with binary coproducts. For any precylinder P on A, the left face map i0 is obtained by composing the coproduct left injection with the cylinder map: i0 = coprod.inl ∘ i.

Русский

Пусть A — объект в категории, где существуют двоичные копродублирования. Для любого прециллиндра P над A левый грань i0 получается как композиция включения левой части копрода coprod.inl с отображением цилиндра i: i0 = coprod.inl ∘ i.

LaTeX

$$$P.i_0 = coprod.inl \circ P.i$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_i : coprod.inl ≫ P.i = P.i₀ := by simp [i]

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