Encodable and Countable instances for Π₀ i, α i #
In this file we provide instances for Encodable (Π₀ i, α i) and Countable (Π₀ i, α i).
instance
instEncodableDFinsuppOfDecidableNeOfNat
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Zero (α i)]
[Encodable ι]
[(i : ι) → Encodable (α i)]
[(i : ι) → (x : α i) → Decidable (x ≠ 0)]
:
Encodable (Π₀ (i : ι), α i)
Equations
- instEncodableDFinsuppOfDecidableNeOfNat = Encodable.ofEquiv ((s : Finset ι) × ((i : { x : ι // x ∈ s }) → { x : α ↑i // x ≠ 0 })) DFinsupp.sigmaFinsetFunEquiv