instFunLike — Mathlib

English

CompactlySupportedContinuousMap has a FunLike structure, i.e., can be treated as functions α → β with pointwise equality and injectivity as usual.

Русский

CompactlySupportedContinuousMap обладает структурой FunLike, т.е. действует как функции α→β с обычной точечной эквивалентностью и инъективностью.

LaTeX

$$CompactlySupportedContinuousMap.instFunLike$$

Lean4

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

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