Theorems · Theorem · general topology
Continuous.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 (c • g)- Defined in
- Mathlib.Topology.Algebra.ConstMulAction
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 and proof · cited by 2,592
- ContinuousConstSMulstatement and proof · cited by 832
- Continuous.compproof · cited by 371
- ContinuousConstSMul.continuous_const_smulproof · cited by 25
Cited by18
Results whose statement or proof uses this declaration.
- Continuous.fun_const_smulproof · cited by 12
- Convex.closureproof · cited by 9
- Continuous.matrix_detproof · cited by 7
- IsCompact.smulproof · cited by 6
- IsCompactOperator.image_subset_compact_of_isVonNBoundedproof · cited by 4
- WithSeminorms.continuous_of_isBoundedproof · cited by 4
- Real.ContinuousOn.circleAverageproof · cited by 2
- NormedSpace.equicontinuous_TFAEproof · cited by 2
- IsCompactOperator.smulproof · cited by 1
- exists_extension_norm_eqproof · cited by 1
- isClosed_setOfPred_map_smulproof · cited by 1
- Seminorm.exists_le_comp_of_isInducingproof · cited by 1