congr_fun — Mathlib

English

If f = g are morphisms, then for any x in the underlying X, f x = g x.

Русский

Если f = g — морфизмы, то для любого x в X выполняется f x = g x.

LaTeX

$$$\forall {X Y : C} {f g : X \to Y} (h : f = g) (x : X), f x = g x$$$

Lean4

/-- Analogue of `congr_fun h x`,
when `h : f = g` is an equality between morphisms in a concrete category.
-/
protected theorem congr_fun {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : ToType X) : f x = g x :=
  congrFun (congrArg (fun k : X ⟶ Y => (k : ToType X → ToType Y)) h) x

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