instFunLike — Mathlib

English

The type of homotopies between two continuous maps carries a natural FunLike structure, i.e., Homotopy f0 f1 can be viewed as a function on I × X into Y.

Русский

Тип гомотопий между двумя непрерывными отображениями имеет естественную структуру FunLike: Homotopy f0 f1 можно рассматривать как функцию на I × X в Y.

LaTeX

$$$\text{FunLike} (\mathrm{Homotopy}(f_0,f_1)) \; (I \times X) \; Y$$$

Lean4

instance instFunLike : FunLike (Homotopy f₀ f₁) (I × X) Y
    where
  coe f := f.toFun
  coe_injective' f g
    h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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