Documentation

Mathlib.Data.Finsupp.Encodable

Encodable and Countable instances for α →₀ β #

In this file we provide instances for Encodable (α →₀ β) and Countable (α →₀ β).

instance instEncodableFinsuppOfDecidableNeOfNat {α : Type u_1} {β : Type u_2} [Encodable α] [Encodable β] [Zero β] [(x : β) → Decidable (x 0)] :
Equations
  • instEncodableFinsuppOfDecidableNeOfNat = Encodable.ofEquiv (Π₀ (x : α), β) finsuppEquivDFinsupp
instance instCountableFinsupp {α : Type u_1} {β : Type u_2} [Countable α] [Countable β] [Zero β] :
Equations
  • =