refl_range

Mathlib.Topology.Path

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

English

The image of the constant path at a is the singleton {a}.

Русский

Образ константного пути в точке a равен {a}.

LaTeX

$$$ \\operatorname{range}(\\text{refl}(a)) = \\{a\\} $$$

Lean4

@[simp]
theorem refl_range {a : X} : range (Path.refl a) = { a } :=
  range_const

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

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

Разделы

Аффилиация

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