extend_range

Mathlib.Topology.Path

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

English

For any path γ from a to b, the image of its extension has the same range as the image of γ itself.

Русский

Для любого пути γ от a до b образ продолжения γ имеет тот же сам изображение, что и сам γ.

LaTeX

$$$\mathrm{range}(\gamma.extend) = \mathrm{range}(\gamma).$$$

Lean4

@[simp]
theorem extend_range {a b : X} (γ : Path a b) : range γ.extend = range γ :=
  IccExtend_range _ γ

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

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

Разделы

Аффилиация

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