congr — Mathlib

English

If f1 = f2, then the induced maps on morphisms after pulling back φ via h coincide; i.e., F f1 φ = F f2 (h ▸ φ).

Русский

Если f1 = f2, тогда отображения, получаемые из них на morphisms совпадают после переноса φ по h.

LaTeX

$$F f1 φ = F f2 (h ▸ φ)$$

Lean4

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

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