homFamily_arrow_mk — Mathlib

English

If X, Y are objects and f: X ⟶ Y with P f, then the homFamily evaluated at the element ⟨Arrow.mk f, hf⟩ equals f. This shows the consistency with Arrow.mk.

Русский

Пусть X, Y — объекты, f: X ⟶ Y и hf: P f. Тогда homFamily на элементе ⟨Arrow.mk f, hf⟩ возвращает f. Это согласованность с конструктором Arrow.mk.

LaTeX

$$$P\,\mathrm{homFamily}(\langle \mathrm{Arrow.mk} f, hf \rangle) = f$$$

Lean4

@[simp]
theorem homFamily_arrow_mk {X Y : C} (f : X ⟶ Y) (hf : P f) : P.homFamily ⟨Arrow.mk f, hf⟩ = f :=
  rfl

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