target_mem_range

Mathlib.Topology.Path

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

English

The target point y of a path γ lies in the image of γ.

Русский

Целевая точка y пути γ лежит в образе γ.

LaTeX

$$$ y \\in \\operatorname{range}(\\gamma) $$$

Lean4

@[simp high]
theorem target_mem_range (γ : Path x y) : y ∈ range ⇑γ :=
  ⟨1, Path.target γ⟩

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

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

Разделы

Аффилиация

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