unique_single — Mathlib

English

If α has a Unique instance, then every x ∈ α →₀ M equals the singleton at the unique element with value x(unique).

Русский

Если у типа α есть уникальный элемент, то каждый x ∈ α →₀ M равен единичному функция с единственным элементом и значением x(уникальный).

LaTeX

$$$x = \mathrm{single}(u, x(u))$, где $u$ — единственный элемент типа $\alpha$$$

Lean4

theorem unique_single [Unique α] (x : α →₀ M) : x = single default (x default) :=
  ext <| Unique.forall_iff.2 single_eq_same.symm

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