refl_extend

Mathlib.Topology.Path

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

English

The extension of the constant path at a is the constant path at a, i.e., extending a constant path yields the same constant path.

Русский

Расширение константного пути в точке a даёт тот же константный путь в a.

LaTeX

$$$(\mathrm{Path.refl}\ a).\mathrm{extend} = \mathrm{Path.const}_{\mathbb{R}}(a)$$$

Lean4

@[simp]
theorem refl_extend {a : X} : (Path.refl a).extend = .const ℝ a :=
  rfl

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

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

Разделы

Аффилиация

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