ext₁ — Mathlib

English

General extensionality for zero-level arrows: equality follows from pointwise equality of endpoints.

Русский

Обобщённая экстенциональность нулевого уровня: равенство следует из покоординатного равенства концов.

LaTeX

$$$\forall {F G : ComposableArrows\ C\ 0}, F.obj' 0 = G.obj 0 \Rightarrow F = G$$$

Lean4

theorem ext₁ {F G : ComposableArrows C 1} (left : F.left = G.left) (right : F.right = G.right)
    (w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom right.symm) : F = G :=
  Functor.ext_of_iso (isoMk₁ (eqToIso left) (eqToIso right) (by simp [map'_eq_hom₁, w]))
    (fun i => by fin_cases i <;> assumption) (fun i => by fin_cases i <;> rfl)

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