range_segment

Mathlib.Analysis.Convex.PathConnected

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

← MathLib Explorer

English

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

Русский

Путь сегмента от a к a равен рефлексивному пути в точке a.

LaTeX

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

Lean4

@[simp]
theorem range_segment (a b : E) : Set.range (Path.segment a b) = [a -[ℝ] b] :=
  by
  rw [segment_eq_image_lineMap, image_eq_range]
  simp only [← segment_apply]

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

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

Разделы

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

Аффилиация

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