punit_ext' — Mathlib

English

Any two functors from any category to the discrete PUnit category are equal.

Русский

Любые два функторов из любой категории в дискретную категорию PUnit равны.

LaTeX

$$$\forall \mathcal{C},\; F,G: \mathcal{C} \to \mathrm{Discrete}\, PUnit \Rightarrow F = G$$$

Lean4

/-- Any two functors to `Discrete PUnit` are *equal*.
You probably want to use `punitExt` instead of this. -/
theorem punit_ext' (F G : C ⥤ Discrete PUnit.{w + 1}) : F = G :=
  Functor.ext fun X => by simp only [eq_iff_true_of_subsingleton]

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