instContinuousEvalElemRealUnitInterval

Mathlib.Topology.Path

URI: https://scilib.ai/kg/mathlib#Path.instContinuousEvalElemRealUnitInterval

English

There exists a canonical continuous evaluation map ev: Path x y × I → X given by ev(γ,t) = γ(t).

Русский

Существуют канонические отображения оценки ev: Path x y × I → X, задаваемое ev(γ,t) = γ(t).

LaTeX

$$$ ev(\\gamma,t) = \\gamma(t) $$$

Lean4

instance : ContinuousEval (Path x y) I X :=
  .of_continuous_forget continuous_induced_dom

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

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

Разделы

Аффилиация

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