coe_restrict

Mathlib.Topology.ContinuousMap.Bounded.Basic

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

English

The coe of f.restrict s equals f restricted to s via the inclusion map.

Русский

Образ отображения f.restrict s совпадает с ограниченной функцией через включение.

LaTeX

$$coe_restrict (f : α →ᵇ β) (s : Set α) : ⇑(f.restrict s) = f ∘ (↑)$$

Lean4

@[simp]
theorem coe_restrict (f : α →ᵇ β) (s : Set α) : ⇑(f.restrict s) = f ∘ (↑) :=
  rfl

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

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

Разделы

Аффилиация

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