instFunLike — Mathlib

English

The family of zero-at-infinity continuous maps C₀(α, β) carries a canonical FunLike structure: functions coerce to their underlying maps via toFun, and this coercion is injective.

Русский

Множество нулевой на бесконечности непрерывных отображений C₀(α, β) обладает канонической структурой FunLike: отображения приводятся к своим базовым отображениям через toFun, и это преобразование инъективно.

LaTeX

$$$ \text{instFunLike}:\; FunLike C_0(\alpha, \beta) \;\alpha\; \beta \quad\text{with } \text{coe } f = f.toFun $$$

Lean4

instance instFunLike : FunLike C₀(α, β) α β where
  coe f := f.toFun
  coe_injective' f g
    h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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