instFunLike — Mathlib

English

Two paths with the same underlying function are equal; i.e., extensionality of paths holds.

Русский

Два пути с одной и той же функцией-основы равны; расширение путей справедливо.

LaTeX

$$$\forall \gamma_1, \gamma_2 : Path\ x\ y,\ (\gamma_1 : I \to X) = \gamma_2 \Rightarrow \gamma_1 = \gamma_2$$$

Lean4

instance instFunLike : FunLike (Path x y) I X
    where
  coe γ := ⇑γ.toContinuousMap
  coe_injective' γ₁ γ₂
    h := by
    simp only [DFunLike.coe_fn_eq] at h
    cases γ₁; cases γ₂; congr

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