ext

Mathlib.Topology.Homotopy.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.Homotopy.ext

English

Let F,G be homotopies from f0 to f1. If F(t,x) = G(t,x) for all (t,x) in I × X, then F = G.

Русский

Пусть F и G – гомотопии от f0 к f1. Если F(t,x) = G(t,x) для всех (t,x) в I × X, то F = G.

LaTeX

$$$\forall F,G:\,\mathrm{Homotopy}(f_0,f_1),\; \forall (t,x)\in I\times X,\ F(t,x)=G(t,x) \Rightarrow F=G$$$

Lean4

@[ext]
theorem ext {F G : Homotopy f₀ f₁} (h : ∀ x, F x = G x) : F = G :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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