restrict_def

Mathlib.Data.Set.Restrict

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

English

For any f : α → β and s ⊆ α, the restricted function s.restrict f is equal to f composed with the inclusion Subtype.val.

Русский

Для любой функции f: α → β и множества s ⊆ α, ограниченная функция s.restrict f равна f ∘ Subtype.val.

LaTeX

$$$s.restrict f = f \circ \operatorname{Subtype.val}$$$

Lean4

theorem restrict_def (s : Set α) : s.restrict (π := π) = fun f x ↦ f x :=
  rfl

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

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

Разделы

Аффилиация

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