Dependent finitely supported functions

Construct a DFinsupp from a dependent function with finite support.

noncomputable def TauCeti.dfinsuppOfFiniteSupport {I : Type u_1} {β : I → Type u_2} [(i : I) → Zero (β i)] (f : (i : I) → β i) (hf : {i : I | f i ≠ 0}.Finite) : Π₀ (i : I), β i

A dependent function with finite support, regarded as a dependent finitely supported function.

Equations

• TauCeti.dfinsuppOfFiniteSupport f hf = DFinsupp.mk hf.toFinset fun (i : ↑↑hf.toFinset) => f ↑i

@[simp]

theorem TauCeti.dfinsuppOfFiniteSupport_apply {I : Type u_1} {β : I → Type u_2} [(i : I) → Zero (β i)] (f : (i : I) → β i) (hf : {i : I | f i ≠ 0}.Finite) (i : I) : (dfinsuppOfFiniteSupport f hf) i = f i

Evaluating dfinsuppOfFiniteSupport f hf returns the original function f.