apply

Mathlib.Topology.ContinuousMap.Defs

URI: https://scilib.ai/kg/mathlib#ContinuousMap.Simps.apply

English

The Simps.apply projection sends a continuous map to its underlying function: apply (f : C(X,Y)) = f.

Русский

Проекция Simps.apply переводит непрерывную карту в её базовую функцию: apply(f) = f.

LaTeX

$$$\\text{ContinuousMap.Simps.apply}(f) = f$$$

Lean4

/-- See note [custom simps projection]. -/
def apply (f : C(X, Y)) : X → Y :=
  f

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

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

Разделы

Аффилиация

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