update_self

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.update_self

English

For any f ∈ Π₀ i, β i and index i, updating the i-th coordinate to f(i) yields f: f.update i (f i) = f.

Русский

Для любой функции f ∈ Π₀ i, β i и индексa i обновление i-й координаты до f(i) даёт ту же функцию: f.update i (f i) = f.

LaTeX

$$$ f.update i (f i) = f $$$

Lean4

@[simp]
theorem update_self : f.update i (f i) = f := by
  ext
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru