hasZeroObject — Mathlib

English

The category of SemiNormedGrp₁ has a zero object, obtained by the one-point normed group PUnit and isZero_of_subsingleton.

Русский

У категории SemiNormedGrp₁ существует нулевой объект, который задаётся однопунктовой нормированной группой PUnit и свойством isZero_of_subsingleton.

LaTeX

$$\\text{Limits.HasZeroObject SemiNormedGrp₁}$$

Lean4

instance hasZeroObject : Limits.HasZeroObject SemiNormedGrp₁.{u} :=
  ⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩

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