Enumeration of a countable local direct sum

noncomputable def Wallace.countableFinsuppEnumeration {I : Type u} {R : Type v} [Zero R] [Countable R] (D : Set I) (hD : D.Countable) : ℕ → ↑D →₀ R

A fixed surjective enumeration of the direct sum over a countable coordinate set.

Equations

• Wallace.countableFinsuppEnumeration D hD = Classical.choose ⋯

theorem Wallace.countableFinsuppEnumeration_surjective {I : Type u} {R : Type v} [Zero R] [Countable R] (D : Set I) (hD : D.Countable) : Function.Surjective (countableFinsuppEnumeration D hD)