Theorems · Theorem · Lie groups
tendsto_mul
∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {a b : M},
Filter.Tendsto (fun p => p.1 * p.2) (nhds (a, b)) (nhds (a * b))- Defined in
- Mathlib.Topology.Algebra.Monoid
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- ContinuousMulstatement and proof · cited by 343
- continuous_iff_continuousAtproof · cited by 139
- ContinuousMul.continuous_mulproof · cited by 3
Cited by7
Results whose statement or proof uses this declaration.
- compact_open_separated_mul_rightproof · cited by 2
- exists_open_nhds_one_splitproof · cited by 2
- HasProd.sumproof · cited by 2
- exists_mem_nhds_zero_mul_subsetproof · cited by 1
- MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendstoproof · cited by 1