eq_const_of_unique — Mathlib

English

If α has a unique element and f: α → β, then f is constant, equal to f(default).

Русский

Если у α есть единственный элемент и функция f: α → β, то f константна и равна f(значение по умолчанию).

LaTeX

$$$f = \\mathrm{const}_{\\\\alpha}(f(\\\\mathrm{default}))$$$

Lean4

theorem eq_const_of_unique {β : Sort*} [Unique α] (f : α → β) : f = Function.const α (f default) :=
  eq_const_of_subsingleton ..

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