∀ {α : Type u_1} {β : Type u_2} {ι : Type u_6} [inst : LinearOrder ι] {f : Filter α} {g : Filter β} {s : ι → Set α}
  {t : ι → Set β}, f.HasAntitoneBasis s → g.HasAntitoneBasis t → (f ×ˢ g).HasAntitoneBasis fun n => s n ×ˢ t n