congr — Mathlib

English

If f1 = f2, then for any φ, the value of a given construction F at f1 and φ equals the value at f2 and the transported φ.

Русский

Если f1 = f2, то для любого φ значение конструктора F в точках f1 и φ равно значению в точке f2 и транспорте φ.

LaTeX

$$$$ F f_1 \\phi = F f_2 (h \\triangleright \\phi) \\quad \\text{when } h: f_1 = f_2. $$$$

Lean4

theorem congr {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : (Action.res _ f₁).obj A ⟶ B} {T : Type*}
    (F : (f : G →* H) → (φ : (Action.res _ f).obj A ⟶ B) → T) : F f₁ φ = F f₂ (h ▸ φ) :=
  by
  subst h
  rfl

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