ext — Mathlib

English

In the over category, morphisms are determined by their left component; two morphisms are equal if their left parts are equal.

Русский

В категории Over морфизмы задаются по левому компоненту; два морфизма равны, если их левые части равны.

LaTeX

$$$\\forall U,V: \\mathrm{Over}(X),\\forall f,g:\\,U\\to V,\\ f.\\text{left}=g.\\text{left} \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext {X : T} {U V : Over X} {f g : U ⟶ V} (h : f.left = g.left) : f = g :=
  by
  let ⟨_, b, _⟩ := f
  let ⟨_, e, _⟩ := g
  congr
  simp only [eq_iff_true_of_subsingleton]

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