ext — Mathlib

English

The morphisms in Under X are determined by their right component; two arrows with the same right component are equal.

Русский

О arrow в категории Under X определяется своей правой частью; у двух стрелок с одинаковой правой частью должны совпадать все данные.

LaTeX

$$$f.right = g.right \\Rightarrow f = g.$$$

Lean4

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

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