English
If l is disjoint from cocompact on M×M, then the product map tends to 0 along (𝓝 0) ⊓ l after a suitable lifting to a coprod-inf structure.
Русский
Если l не пересекается кококомпакт на M×M, умножение стремится к 0 вдоль (𝓝 0) ⊓ l после подходящей переработки в инф-операцию.
LaTeX
$$tendsto_mul_coprod_nhds_zero_inf_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 × M` which is disjoint from the cocompact filter. Then, the multiplication
map `M × M → M` tends to zero on `(𝓝 0).coprod (𝓝 0) ⊓ l`. -/
theorem tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact {l : Filter (M × M)}
(hl : Disjoint l (cocompact (M × M))) : Tendsto (fun x : M × M ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0) :=
by
have :=
calc
(𝓝 0).coprod (𝓝 0) ⊓ l
_ ≤ (𝓝 0).coprod (𝓝 0) ⊓ map Prod.fst l ×ˢ map Prod.snd l := (inf_le_inf_left _ le_prod_map_fst_snd)
_ ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0 := coprod_inf_prod_le _ _ _ _
apply (Tendsto.sup _ _).mono_left this
· apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
exact disjoint_map_cocompact continuous_snd hl
· apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
exact disjoint_map_cocompact continuous_fst hl
