isZero_of_subsingleton — Mathlib

English

If a SemiNormedGrp₁ object V has at most one element (is subsingleton), then V is a zero object in the category: there is a unique morphism from any object to V and from V to any object.

Русский

Если у V имеется не более одного элемента (subs singleton), то V является нулевым объектом в категории: для любого X существует и единственный морфизм X → V и V → X.

LaTeX

$$\\text{Subsingleton}(V) \\Rightarrow \\text{Limits.IsZero}(V)$$

Lean4

theorem isZero_of_subsingleton (V : SemiNormedGrp₁) [Subsingleton V] : Limits.IsZero V :=
  by
  refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
  · ext x; have : x = 0 := Subsingleton.elim _ _; simp only [this, map_zero]
  · ext; apply Subsingleton.elim

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