hom_inl_inr_false — Mathlib

English

In the sum of two categories, there are no morphisms from an object in the left component to an object in the right component.

Русский

В сумме двух категорий нет морфизмов между объектами из левой и правой компонент.

LaTeX

$$$$ (\mathrm{Sum}\; C\; D).\mathrm{Hom}(\mathrm{inl} X, \mathrm{inr} Y) = \emptyset. $$$$

Lean4

@[aesop norm -10 destruct (rule_sets := [CategoryTheory])]
theorem hom_inl_inr_false {X : C} {Y : D} (f : Sum.inl X ⟶ Sum.inr Y) : False := by cases f

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