of_eq — Mathlib

English

If f: X ⟶ Y lies in P and X' = X, Y' = Y via equalities hX, hY, and f' is obtained from f by transporting along these equalities, then P f'. This expresses invariance under transporting endpoints along equalities.

Русский

Если f: X ⟶ Y принадлежит P и X' = X, Y' = Y посредством равенств hX, hY, и f' получается из f перенесением вдоль этих равенств, тогда P f'.

LaTeX

$$If f' = (eqToHom hX.symm) ≫ f ≫ (eqToHom hY) with hf: P f, then P f'.$$

Lean4

theorem of_eq {X Y : C} {f : X ⟶ Y} (hf : P f) {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y')
    (h : f' = eqToHom hX.symm ≫ f ≫ eqToHom hY) : P f' :=
  by
  rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢
  rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]

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