lift_eq — Mathlib

English

Compatibility between lift and desc expressed as a simplification: a lift followed by a desc equals the sum of the pairwise compositions with f and g.

Русский

Свойство совместимости lift и desc: lift f g ≫ desc h i = f ≫ h + g ≫ i.

LaTeX

$$$\operatorname{biproduct.lift} f g \;\gg\; \operatorname{biproduct.desc} h i = f \GGArrow h + g \GGArrow i$$$

Lean4

theorem lift_eq {T : C} {f : T ⟶ X} {g : T ⟶ Y} : biprod.lift f g = f ≫ biprod.inl + g ≫ biprod.inr := by
  ext <;> simp [add_comp]

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