delayReflLeft_one

Mathlib.Topology.Homotopy.HSpaces

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

English

DelayReflLeft(1, γ) equals γ.

Русский

DelayReflLeft(1, γ) = γ.

LaTeX

$$delayReflLeft(1, γ) = γ$$

Lean4

theorem delayReflLeft_one (γ : Path x y) : delayReflLeft 1 γ = γ := by
  simp only [delayReflLeft, delayReflRight_one, Path.symm_symm]

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

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

Разделы

Аффилиация

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