congr_arg

Mathlib.Topology.Homotopy.Basic

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

English

If F=G, then F(x) = G(x) for all x in I×X.

Русский

Если F=G, то F(x)=G(x) для всех x в I×X.

LaTeX

$$$F=G \Rightarrow F(x)=G(x)\quad(\forall x:\; I\times X)$$$

Lean4

protected theorem congr_arg (F : Homotopy f₀ f₁) {x y : I × X} (h : x = y) : F x = F y :=
  F.toContinuousMap.congr_arg h

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

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

Разделы

Аффилиация

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