restrict_def

Mathlib.Data.Finset.Pi

URI: https://scilib.ai/kg/mathlib#Finset.restrict_def

English

Restriction to a finite set s coincides with the natural restriction to the corresponding set-valued type.

Русский

Ограничение до множества s совпадает с естественным ограничением к соответствующему множеству значений.

LaTeX

$$$ s.\\restrict(\\pi) = \\lambda f x. f x.$$$

Lean4

theorem restrict_def (s : Finset ι) : s.restrict (π := π) = fun f x ↦ f x :=
  rfl

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

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

Разделы

Аффилиация

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