restrict_apply

Mathlib.Topology.ContinuousMap.Bounded.Basic

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

English

Restricting f to s and evaluating at x ∈ s yields the same value as evaluating f at x.

Русский

Ограничение f на s и вычисление в точке x ∈ s дают такое же значение, как и вычисление f в x.

LaTeX

$$restrict_apply (f : α →ᵇ β) (s : Set α) (x : s) : (f.restrict s) x = f x$$

Lean4

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

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

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

Разделы

Аффилиация

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