Theorems · Theorem · Lie groups

tendsto_mul_cofinite_nhds_zero

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

If f : α → M and g : β → M both tend to zero on the cofinite filter, then so does fun i : α × β ↦ f i.1 * g i.2.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMulZeroClassContinuousMul