update_eq_const_of_subsingleton — Mathlib

English

If the domain α is a Subsingleton, then for any a and any v and any f : α → α', the update f a v is the constant function v.

Русский

Если множество домена является подсущностным, то обновление f в точке a значением v есть константная функция, равная v на всём множестве.

LaTeX

$$$[Subsingleton\\ \\alpha]\\ (a:\\alpha)\n\\ (v:\\alpha')\\ (f:\\alpha\\to\\alpha'):\\n update\\ f\\ a\\ v = \\mathrm{const}_{\\alpha} v$$

Lean4

@[nontriviality]
theorem update_eq_const_of_subsingleton [Subsingleton α] (a : α) (v : α') (f : α → α') : update f a v = const α v :=
  funext fun a' ↦ Subsingleton.elim a a' ▸ update_self ..

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