extend_cast

Mathlib.Topology.Path

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

English

Extending a path commutes with casting: (γ.cast hx hy).extend = γ.extend.

Русский

Продление пути коммутирует с приведением: (γ.cast hx hy).extend = γ.extend.

LaTeX

$$$(\gamma.cast hx hy).extend = \gamma.extend$$$

Lean4

@[simp]
theorem extend_cast {x' y'} (γ : Path x y) (hx : x' = x) (hy : y' = y) : (γ.cast hx hy).extend = γ.extend :=
  rfl

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

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

Разделы

Аффилиация

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