inr_i — Mathlib

English

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

Русский

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

LaTeX

$$$P.i_1 = coprod.inr \circ P.i$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_i : coprod.inr ≫ P.i = P.i₁ := by simp [i]

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