single_eq_pi_single

Mathlib.Data.Finsupp.Single

URI: https://scilib.ai/kg/mathlib#Finsupp.single_eq_pi_single

English

For DecidableEq α, the function single a b equals Pi.single a b.

Русский

При допускаемой в теории эквивалентности α, single a b равна Pi.single a b.

LaTeX

$$$$\\text{For }[\\text{DecidableEq } \\alpha],\\; \\text{single } a\\, b = \\Pi.single\\, a\\, b.$$$$

Lean4

theorem single_eq_pi_single [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Pi.single a b :=
  single_eq_update a b

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

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

Разделы

Аффилиация

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