English
Definition of the induction principle for morphisms in the sum category: to prove a property P for a morphism f : X ⟶ Y in Sum C D it suffices to prove P for the case X,Y both in C and f coming from C, or for the case X,Y both in D with f coming from D.
Русский
Определение принципа индукции по морфизмам в сумме категорий: чтобы доказать свойство P для морфизма f : X ⟶ Y в Sum C D, достаточно доказать P для случаев, когда обе стороны в C и морфизм происходит из C, или когда обе стороны в D и морфизм из D.
LaTeX
$$$$ \mathrm{Sum}.homInduction : \ldots $$$$
Lean4
@[simp]
theorem homInduction_left {P : {x y : C ⊕ D} → (x ⟶ y) → Sort*} (inl : ∀ x y : C, (f : x ⟶ y) → P ((inl_ C D).map f))
(inr : ∀ x y : D, (f : x ⟶ y) → P ((inr_ C D).map f)) {x y : C} (f : x ⟶ y) :
homInduction inl inr ((inl_ C D).map f) = inl x y f :=
rfl
