ext — Mathlib

English

For any morphism f: P ⟶ Q in Karoubi C, P.p ≫ f.f = f.f.

Русский

Для любого морфизма f: P ⟶ Q в Karoubi C выполняется P.p ≫ f.f = f.f.

LaTeX

$$P.p ≫ f.f = f.f$$

Lean4

@[ext (iff := false)]
theorem ext {P Q : Karoubi C} (h_X : P.X = Q.X) (h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p) : P = Q :=
  by
  cases P
  cases Q
  dsimp at h_X h_p
  subst h_X
  simpa only [mk.injEq, heq_eq_eq, true_and, eqToHom_refl, comp_id, id_comp] using h_p

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