instCoeFunForall

Mathlib.Topology.Homotopy.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousMap.HomotopyEquiv.instCoeFunForall

English

A homotopy equivalence X ≃ₕ Y can be viewed as a function X → Y.

Русский

Гомотопическая эквивалентность X ≃ₕ Y можно рассматривать как отображение X → Y.

LaTeX

$$$(X\simeq_h Y) \Rightarrow (X \to Y).$$$

Lean4

instance : CoeFun (X ≃ₕ Y) fun _ => X → Y :=
  ⟨fun f => f.toFun⟩

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

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

Разделы

Аффилиация

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