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

instance instCountableDFinsupp {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [Countable ι] [∀ (i : ι), Countable (α i)] : Countable (Π₀ (i : ι), α i)