segment_same

Mathlib.Analysis.Convex.PathConnected

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

English

The segment from a to a is identically equal to the reflexive path at a.

Русский

Сегмент от a к a совпадает с рефлексивным путём в a повсеместно.

LaTeX

$$$\text{Path.segment}(a,a)=\text{Path.refl}(a)$$$

Lean4

@[simp]
protected theorem segment_same (a : E) : Path.segment a a = .refl a := by ext; simp

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

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

Разделы

Аффилиация

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