map₂_eqToHom — Mathlib

English

Let F be a PrelaxFunctor. For any f,g: x ⟶ y with hfg: f = g, the image of eqToIso hfg under map₂ is the iso between F.map f and F.map g induced by hfg.

Русский

Пусть F — Прелакс-функтор. Для любых стрелок f,g: x ⟶ y с hfg: f = g отображение eqToIso hfg через map₂ есть изо между F.map f и F.map g, вызываемое этим равенством.

LaTeX

$$$\forall {B,C} (F: B \to C) \; \forall x,y: B \; \forall f,g: x \to y \; (hfg: f = g),\ F.map₂(\mathbf{eqToIso}(hfg)) = \mathbf{eqToIso}(\\text{by rw} [\\lhd \! hfg \!] )$$$

Lean4

theorem map₂_eqToHom {x y : B} (f g : x ⟶ y) (hfg : f = g) : F.map₂ (eqToHom hfg) = eqToHom (by rw [← hfg]) :=
  by
  subst hfg
  simp

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