homInduction_left — Mathlib

English

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

Русский

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

LaTeX

$$homInduction\\_left = left$$

Lean4

@[simp]
theorem homInduction_left {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 : C}
    (f : x ⟶ y) : homInduction left right edge ((inclLeft C D).map f) = left x y f :=
  rfl

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