Documentation

Mathlib.Data.DFinsupp.Encodable

Encodable and Countable instances for Π₀ i, α i #

In this file we provide instances for Encodable (Π₀ i, α i) and Countable (Π₀ i, α i).

instance instEncodableDFinsupp {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [Encodable ι] [(i : ι) → Encodable (α i)] [(i : ι) → (x : α i) → Decidable (x 0)] :
Encodable (Π₀ (i : ι), α i)
Equations
  • instEncodableDFinsupp = 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)
Equations