Theorems · Theorem · Lie groups
ContinuousSMul.continuous_smul
∀ {M : Type u_1} {X : Type u_2} {inst : SMul M X} {inst_1 : TopologicalSpace M} {inst_2 : TopologicalSpace X}
[self : ContinuousSMul M X], Continuous fun p => p.1 • p.2The scalar multiplication (•) is continuous.
- Defined in
- Mathlib.Topology.Algebra.MulAction
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ContinuousSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- ContinuousSMulstatement and proof · cited by 1,016
Cited by21
Results whose statement or proof uses this declaration.
- Filter.Tendsto.smulproof · cited by 22
- Continuous.smulproof · cited by 17
- MeasureTheory.AEStronglyMeasurable.smulproof · cited by 14
- IsScalarTower.continuousSMulproof · cited by 8
- aeconst_of_dense_setOfPred_preimage_smul_aeproof · cited by 4
- balancedCore_mem_nhds_zeroproof · cited by 4
- MeasureTheory.StronglyMeasurable.smulproof · cited by 3
- MeasureTheory.StronglyMeasurable.smul_constproof · cited by 3
- Topology.IsInducing.continuousMulproof · cited by 2
- smul_set_closure_subsetproof · cited by 2
- IsCompact.smul_setproof · cited by 2
- MeasureTheory.Integrable.smul_prodproof · cited by 2