restrict_apply

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.restrict_apply

English

For any f and s, and x in s, (f.restrict s) x = f x.

Русский

Для любого f и s, и для x в s, (f.restrict s) x = f x.

LaTeX

$$$\forall f: C(\alpha,\beta)\,\forall s\subseteq \alpha\,\forall x\in s:\ (f\restriction s)(x)=f(x)$$$

Lean4

@[simp]
theorem restrict_apply (f : C(α, β)) (s : Set α) (x : s) : f.restrict s x = f x :=
  rfl

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

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

Разделы

Аффилиация

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