Theorems · Theorem · general topology
ContinuousConstSMul.continuous_const_smul
∀ {Γ : Type u_1} {T : Type u_2} {inst : TopologicalSpace T} {inst_1 : SMul Γ T} [self : ContinuousConstSMul Γ T]
(γ : Γ), Continuous fun x => γ • xThe scalar multiplication (•) : Γ → T → T is continuous in the second argument.
- Defined in
- Mathlib.Topology.Algebra.ConstMulAction
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- ContinuousConstSMul
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
- ContinuousConstSMulstatement and proof · cited by 832
Cited by25
Results whose statement or proof uses this declaration.
- Continuous.const_smulproof · cited by 18
- Filter.Tendsto.const_smulproof · cited by 13
- HasSum.const_smulproof · cited by 11
- IsQuotientCoveringMap.monodromy_toPermFiberproof · cited by 3
- ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_selfproof · cited by 3
- smul_closure_subsetproof · cited by 3
- IsCompact.locallyCompactSpace_of_mem_nhds_of_groupproof · cited by 2
- Submodule.mapsTo_smul_closureproof · cited by 2
- continuous_skewAdjointPartproof · cited by 1
- NormedSpace.exp_smulproof · cited by 1
- Real.uniformContinuous_const_mulproof · cited by 1
- Balanced.closureproof · cited by 1