Theorems · Theorem · Lie groups
continuous_mul_const
∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] (m : M),
Continuous fun x => x * m- Defined in
- Mathlib.Topology.Algebra.Monoid.Defs
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Continuousstatement · cited by 2,592
- SeparatelyContinuousMulstatement and proof · cited by 133
- SeparatelyContinuousMul.continuous_mul_constproof · cited by 1
Cited by31
Results whose statement or proof uses this declaration.
- Filter.Tendsto.mul_constproof · cited by 23
- Continuous.mul_constproof · cited by 15
- Complex.continuous_cosproof · cited by 7
- Complex.continuous_sinproof · cited by 5
- ContinuousMap.mulRightproof · cited by 4
- Set.isClosed_centralizerproof · cited by 4
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- IsMIntegralCurveOn.comp_mulproof · cited by 3
- MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactorproof · cited by 3
- ContinuousMultilinearMap.isLeast_opNormproof · cited by 2
- continuousAt_clogproof · cited by 2