English
Let l be a filter with Disjoint l (cocompact M); if l ≤ (nhds 0) ⊓ (nhds 0), then Tendsto (x.fst * x.snd) l (nhds 0).
Русский
Пусть l диссоциирован с кококомпакт; если l ≤ (nhds 0) ⊓ (nhds 0), то сходится к 0 функция умножения на пары.
LaTeX
$$Tendsto (fun x : M × M ↦ x.1 * x.2) l (nhds 0)$$
Lean4
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M × M` which is both disjoint from the cocompact filter and less than or
equal to `(𝓝 0).coprod (𝓝 0)`. Then the multiplication map `M × M → M` tends to zero on `l`. -/
theorem tendsto_mul_nhds_zero_of_disjoint_cocompact {l : Filter (M × M)} (hl : Disjoint l (cocompact (M × M)))
(h'l : l ≤ (𝓝 0).coprod (𝓝 0)) : Tendsto (fun x : M × M ↦ x.1 * x.2) l (𝓝 0) := by
simpa [inf_eq_right.mpr h'l] using tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact hl
