instOne — Mathlib

English

There is a canonical constant-one continuous map serving as the identity element.

Русский

Существует каноническое непрерывное отображение, константное в единицу, являющееся тождественным элементом.

LaTeX

$$There is a constant map 1: C(α, β) with value 1, i.e. the identity element of the monoid of continuous maps.$$

Lean4

@[to_additive]
instance [One β] : One C(α, β) :=
  ⟨const α 1⟩

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