hasZeroObject_pUnit — Mathlib

English

There exists a zero object in the discrete category on PUnit.

Русский

Существование нулевого объекта в дискретной категории на PUnit.

LaTeX

$$$\\\\text{HasZeroObject}(\\\\text{Discrete } PUnit)$$$

Lean4

instance hasZeroObject_pUnit : HasZeroObject (Discrete PUnit) where
  zero :=
    ⟨⟨⟨⟩⟩,
      { unique_to := fun ⟨⟨⟩⟩ => ⟨{ default := 𝟙 _, uniq := by subsingleton }⟩
        unique_from := fun ⟨⟨⟩⟩ => ⟨{ default := 𝟙 _, uniq := by subsingleton }⟩ }⟩

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