Theorems · Theorem · general topology
Continuous.fun_const_smul
∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
[inst_3 : TopologicalSpace β] {g : β → α}, Continuous g → ∀ (c : M), Continuous fun i => c • g iEta-expanded form of Continuous.const_smul
- Defined in
- Mathlib.Topology.Algebra.ConstMulAction
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 9 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 · cited by 24,529
- Continuousstatement · cited by 2,592
- ContinuousConstSMulstatement · cited by 832
- Continuous.const_smulproof · cited by 18
Cited by12
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.addHaarScalarFactor_domSMulproof · cited by 3
- isClosed_setOfPred_convexOnproof · cited by 2
- AffineMap.homothety_continuousproof · cited by 2
- ExistsContDiffBumpBase.y_pos_of_mem_ballproof · cited by 1
- ModularGroup.exists_bound_of_subgroup_invariant_of_isBigOproof · cited by 1
- selfAdjoint.continuous_expUnitaryproof · cited by 0
- Topology.IsInducing.continuousConstSMulproof · cited by 0
- ExistsContDiffBumpBase.y_le_oneproof · cited by 0
- Continuous.inner_proof · cited by 0
- Convex.smul_vadd_mem_of_mem_nhds_of_mem_asymptoticConeproof · cited by 0
- eventually_nhds_norm_smul_sub_ltproof · cited by 0
- Continuous.fourierPowSMulRightproof · cited by 0