Theorems · Theorem · general topology
ContinuousMap.continuous
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)), Continuous ⇑fDeprecated. Use map_continuous instead.
- Defined in
- Mathlib.Topology.ContinuousMap.Defs
- Cited by
- 74 results in Mathlib
- Foundations
- Depth 14 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.
- DFunLike.coestatement · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- Continuousstatement · cited by 2,592
- ContinuousMapstatement and proof · cited by 2,491
- ContinuousMap.continuous_toFunproof · cited by 47
Cited by76
Results whose statement or proof uses this declaration.
- BoundedContinuousFunction.continuousproof · cited by 26
- Path.Homotopic.Quotient.mapproof · cited by 19
- Real.continuous_fourierCharproof · cited by 10
- CompactlySupportedContinuousMap.integrableproof · cited by 9
- IsCoveringMap.eq_liftPath_iff'proof · cited by 5
- Topology.WithGeneratedByTopology.continuous_equivproof · cited by 4
- ContinuousMap.continuous_comp'proof · cited by 4
- Path.Homotopy.mapstatement · cited by 4
- aeconst_of_dense_setOfPred_preimage_smul_aeproof · cited by 4
- aeconst_of_dense_setOfPred_preimage_vadd_aeproof · cited by 4
- IsCoveringMap.exists_path_liftsproof · cited by 4
- isCompact_setOfPred_finiteMeasure_le_of_compactSpaceproof · cited by 3