homOfEq_edge — Mathlib

English

If two isomorphic morphisms have equal edges, the associated edge is preserved under the constructed isomorphism.

Русский

Если два изоморфизма имеют равные рёбра, соответствующее ребро сохраняется в конструируемом изоморфизме.

LaTeX

$$$$ \text{homOfEq}(f,\alpha,\beta).edge = f.edge $$$$

Lean4

@[simp]
theorem homOfEq_edge {X : SSet.Truncated.{u} 2} {x₁ y₁ x₂ y₂ : OneTruncation₂ X} (f : x₁ ⟶ y₁) (hx : x₁ = x₂)
    (hy : y₁ = y₂) : (Quiver.homOfEq f hx hy).edge = f.edge :=
  by
  subst hx hy
  rfl

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