extend_extends

Mathlib.Topology.Path

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

English

See above: persistence of extension under endpoint specification.

Русский

См. выше: сохранение свойства расширения при задании концов.

LaTeX

$$$ γ.extend t = γ ⟨t, ht⟩$$$

Lean4

@[simp]
theorem extend_extends {a b : X} (γ : Path a b) {t : ℝ} (ht : t ∈ (Icc 0 1 : Set ℝ)) : γ.extend t = γ ⟨t, ht⟩ :=
  IccExtend_of_mem _ γ ht

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

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

Разделы

Аффилиация

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