English
Let f: α → M and g: β → M be maps with corresponding tendences to 0 along cocompact filters; then the pointwise product map (i,j) ↦ f(i) g(j) tends to 0 along cocompact on α × β.
Русский
Пусть f: α → M и g: β → M стремятся к 0 по кокомпакт-фильтрам; тогда точечное произведение (i,j) ↦ f(i) g(j) стремится к 0 по кокомпакт на α × β.
LaTeX
$$tendsto_mul_prod_nhds_zero_of_disjoint_cocompact$$
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 `𝓝 0 ×ˢ l`. -/
theorem tendsto_mul_nhds_zero_prod_of_disjoint_cocompact {l : Filter M} (hl : Disjoint l (cocompact M)) :
Tendsto (fun x : M × M ↦ x.1 * x.2) (𝓝 0 ×ˢ l) (𝓝 0) :=
calc
map (fun x : M × M ↦ x.1 * x.2) (𝓝 0 ×ˢ l)
_ ≤ map (fun x : M × M ↦ x.1 * x.2) (𝓝ˢ ({0} ×ˢ Set.univ)) := (map_mono <| nhds_prod_le_of_disjoint_cocompact 0 hl)
_ ≤ 𝓝 0 := continuous_mul.tendsto_nhdsSet_nhds fun _ ⟨hx, _⟩ ↦ mul_eq_zero_of_left hx _
