continuous_extend

Mathlib.Topology.Path

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

English

For any a,b ∈ X, γ : Path a b and t ∈ I, γ.extend t = γ ⟨t, ht⟩ where ht encodes t ∈ Icc 0 1.

Русский

Для любых a,b ∈ X, γ : Path a b и t ∈ I, γ.extend t = γ ⟨t, ht⟩, где ht кодирует t ∈ Icc 0 1.

LaTeX

$$$ γ.extend(t) = γ(\\langle t,ht\\rangle) $$$

Lean4

/-- A useful special case of `Continuous.path_extend`. -/
theorem continuous_extend : Continuous γ.extend :=
  γ.continuous.Icc_extend'

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

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

Разделы

Аффилиация

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