feat: "outer product" of functions that tend to zero on the cocompact filter

[trivial1711]

Let M be a topological space with a continuous multiplication operation and a zero.

We prove that if f : α → M and g : β → M are continuous functions that both tend to zero on the cocompact filter, then the "outer product" fun (i : α × β) ↦ (f i.1) * (g i.2) also tends to zero on the cocompact filter.

We then specialize this result to the case that α and β have the discrete topology.

---

• [x] depends on: #12305