restrict_updateFinset

Mathlib.Data.Finset.Update

URI: https://scilib.ai/kg/mathlib#Function.restrict_updateFinset

← MathLib Explorer

English

Restricting the updated vector yields the original y on s.

Русский

Ограничение обновления даёт исходное y на s.

LaTeX

$$$s.restrict(\\text{updateFinset } x s y) = y$$$

Lean4

theorem restrict_updateFinset {s : Finset ι} (x : Π i, π i) (y : Π i : s, π i) : s.restrict (updateFinset x s y) = y :=
  by
  rw [restrict_updateFinset_of_subset subset_rfl]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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