equivFunOnFinite — Mathlib

English

There is a natural bijection between finitely supported functions α →₀ M and all functions α → M when α is finite.

Русский

Существует естественная биекция между функциями с конечной опорой α →₀ M и всеми функциями α → M, если α конечен.

LaTeX

$$\alpha \text{ finite } \\Rightarrow (\\alpha \\to_0 M) \\cong (\\alpha \\to M)$$

Lean4

/-- Given `Finite α`, `equivFunOnFinite` is the `Equiv` between `α →₀ β` and `α → β`.
  (All functions on a finite type are finitely supported.) -/
@[simps]
def equivFunOnFinite [Finite α] : (α →₀ M) ≃ (α → M)
    where
  toFun := (⇑)
  invFun f := mk (Function.support f).toFinite.toFinset f fun _a => Set.Finite.mem_toFinset _

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