source_mem_range

Mathlib.Topology.Path

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

English

The source point x of a path γ lies in the image of γ.

Русский

Начальная точка x пути γ лежит в образе γ.

LaTeX

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

Lean4

@[simp high]
theorem source_mem_range (γ : Path x y) : x ∈ range ⇑γ :=
  ⟨0, Path.source γ⟩

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

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

Разделы

Аффилиация

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