cast_coe

Mathlib.Topology.Path

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

English

Casting preserves the underlying function. The functions (γ.cast hx hy) and γ have the same evaluation on the unit interval: (γ.cast hx hy : I → X) = γ.

Русский

Приведение сохраняет основанную функцию: (γ.cast hx hy : I → X) = γ.

LaTeX

$$$(\gamma.cast hx hy : I \to X) = \gamma$$$

Lean4

@[simp]
theorem cast_coe (γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : (γ.cast hx hy : I → X) = γ :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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