ext — Mathlib

English

Equality of Arrow morphisms is determined by their components and whiskers.

Русский

Равенство морфизмов стрелы определяется компонентами и whisker-операциями.

LaTeX

$$$\forall f,g : Arrow\ T\; (h_1: f.left = g.left) (h_2: f.right = g.right) (h_3: f.hom = eqToHom h_1 ≫ g.hom ≫ eqToHom h_2^{{\cdot}}) \Rightarrow f = g$$$

Lean4

theorem ext {f g : Arrow T} (h₁ : f.left = g.left) (h₂ : f.right = g.right)
    (h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom h₂.symm) : f = g :=
  (mk_eq_mk_iff _ _).2 (by simp_all)

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