Bases for finite powers of a filter

A basis of a filter gives a basis of uniform cubes for each finite power of that filter.

theorem Filter.HasBasis.pi_self_of_finite {α : Type u_1} {κ : Type u_2} {ι : Type u_3} [Finite ι] {f : Filter α} {p : κ → Prop} {s : κ → Set α} (h : f.HasBasis p s) : (pi fun (x : ι) => f).HasBasis p fun (k : κ) => Set.univ.pi fun (x : ι) => s k

A finite power of a filter has a basis of cubes indexed by the original basis.