Theorems · Theorem · Lie groups

tendsto_mul_cocompact_nhds_zero

∀ {M : Type u_3} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M]
  [inst_3 : TopologicalSpace α] [inst_4 : TopologicalSpace β] {f : α → M} {g : β → M},
  Continuous f →
    Continuous g →
      Filter.Tendsto f (Filter.cocompact α) (nhds 0) →
        Filter.Tendsto g (Filter.cocompact β) (nhds 0) →
          Filter.Tendsto (fun i => f i.1 * g i.2) (Filter.cocompact (α × β)) (nhds 0)

If f : α → M and g : β → M are continuous and both tend to zero on the cocompact filter, then fun i : α × β ↦ f i.1 * g i.2 also tends to zero on the cocompact filter.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceMulZeroClassContinuousMulTopologicalSpaceTopologicalSpace