English
If l is a filter on M that is disjoint from the cocompact filter, then the product map tends to 0 along l × 𝓝 0, under mild hypotheses.
Русский
Если фильтр l не пересекает кококомпакт, умножение по структуре моноида стремится к 0 вдоль l × 𝓝 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` which is disjoint from the cocompact filter. Then, the multiplication map
`M × M → M` tends to zero on the filter product `l ×ˢ 𝓝 0`. -/
theorem tendsto_mul_prod_nhds_zero_of_disjoint_cocompact {l : Filter M} (hl : Disjoint l (cocompact M)) :
Tendsto (fun x : M × M ↦ x.1 * x.2) (l ×ˢ 𝓝 0) (𝓝 0) :=
calc
map (fun x : M × M ↦ x.1 * x.2) (l ×ˢ 𝓝 0)
_ ≤ map (fun x : M × M ↦ x.1 * x.2) (𝓝ˢ (Set.univ ×ˢ {0})) := (map_mono <| prod_nhds_le_of_disjoint_cocompact 0 hl)
_ ≤ 𝓝 0 := continuous_mul.tendsto_nhdsSet_nhds fun _ ⟨_, hx⟩ ↦ mul_eq_zero_of_right _ hx
