unique_ext — Mathlib

English

If α has a unique element, two finitely supported functions f,g: α →₀ M are equal whenever their value at the unique element agrees.

Русский

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

LaTeX

$$Unique α \\Rightarrow (f = g) \\Longleftarrow (f(a_0) = g(a_0))$$

Lean4

@[ext]
theorem unique_ext [Unique α] {f g : α →₀ M} (h : f default = g default) : f = g :=
  ext fun a => by rwa [Unique.eq_default a]

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