ofSupportFinite — Mathlib

English

If f has finite support, there exists a finitely supported function whose underlying function is f and whose support is exactly the support of f.

Русский

Если у f конечная опора, существует функция с конечной опорой, совпадающая с f и чья опора равна опоре f.

LaTeX

$$If (Function.support f).Finite, then there exists φ = (α →₀ M) with toFun φ = f and support φ = support f$$

Lean4

/-- The natural `Finsupp` induced by the function `f` given that it has finite support. -/
noncomputable def ofSupportFinite (f : α → M) (hf : (Function.support f).Finite) : α →₀ M
    where
  support := hf.toFinset
  toFun := f
  mem_support_toFun _ := hf.mem_toFinset

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