extendProp

Mathlib.Topology.Homotopy.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.HomotopyWith.extendProp

English

Propagating the predicate P through the extension of the homotopy preserves P.

Русский

Расширение гомотопии сохраняет свойство P.

LaTeX

$$$\\forall t\\in \\mathbb{R},\\; P\\big(F.toHomotopy.extend t\\big)$$$

Lean4

theorem extendProp (F : HomotopyWith f₀ f₁ P) (t : ℝ) : P (F.toHomotopy.extend t) :=
  F.prop _

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

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

Разделы

Аффилиация

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