Theorems · Theorem · Lie groups
continuous_const_mul
∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] (m : M),
Continuous fun x => m * x- Defined in
- Mathlib.Topology.Algebra.Monoid.Defs
- Cited by
- 47 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_const_mulproof · cited by 1
Cited by48
Results whose statement or proof uses this declaration.
- Filter.Tendsto.const_mulproof · cited by 55
- Continuous.const_mulproof · cited by 27
- Real.continuous_fourierCharproof · cited by 10
- Set.isClosed_centralizerproof · cited by 4
- ContinuousMap.mulLeftproof · cited by 3
- LinearMap.norm_extendOfNorm_apply_leproof · cited by 3
- ApproximatesLinearOn.norm_fderiv_sub_leproof · cited by 3
- Commute.cfcHomproof · cited by 2
- Commute.cfcₙHomproof · cited by 2
- IsTopologicalGroup.continuous_conjproof · cited by 2
- Function.Periodic.continuous_qParamproof · cited by 2
- TorusIntegrable.function_integrableproof · cited by 2