homInduction_right — Mathlib

English

For any left and right induction rules, the value of homInduction applied to a right morphism equals the right rule applied to the morphism on the right side.

Русский

Для правой индукции значение функции homInduction совпадает с применением правого правила к морфизму справа.

LaTeX

$$homInduction\\_right = right$$

Lean4

@[simp]
theorem homInduction_right {P : {x y : C ⋆ D} → (x ⟶ y) → Sort*}
    (left : ∀ x y : C, (f : x ⟶ y) → P ((inclLeft C D).map f))
    (right : ∀ x y : D, (f : x ⟶ y) → P ((inclRight C D).map f)) (edge : ∀ (c : C) (d : D), P (edge c d)) {x y : D}
    (f : x ⟶ y) : homInduction left right edge ((inclRight C D).map f) = right x y f :=
  rfl

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