congr_fun

Mathlib.Topology.Homotopy.Basic

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

English

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

Русский

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

LaTeX

$$$F=G \Rightarrow \forall x\in I\times X,\ F(x)=G(x)$$$

Lean4

protected theorem congr_fun {F G : Homotopy f₀ f₁} (h : F = G) (x : I × X) : F x = G x :=
  ContinuousMap.congr_fun (congr_arg _ h) x

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

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

Разделы

Аффилиация

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