Structures · Topology
ContinuousMapClass
ContinuousMapClass F X Y states that F is a type of continuous maps.
You should extend this class when you extend ContinuousMap.
- Defined in
- Mathlib.Topology.ContinuousMap.Defs
- Shape
- 3 explicit arguments · adds map_continuous
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by8
Concrete types that are instances17
- ContinuousMapZero
- ContMDiffMap
- ContinuousAlternatingMap
- ContinuousMultilinearMap
- SchwartzMap
- ContinuousAffineMap
- NormedAddGroupHom
- PontryaginDual
- ContinuousAddMonoidHom
- ContinuousMonoidHom
- Path
- Homeomorph
- ContinuousAlgHom
- ContMDiffAddMonoidMorphism
- ContMDiffMonoidMorphism
- Diffeomorph
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by45
- ContinuousMapClass.map_continuous
- toContinuousMap
- ContinuousAddMonoidHom.toContinuousAddMonoidHom
- Bundle.Trivialization.pullback
- ContinuousMonoidHom.toContinuousMonoidHom
- toContinuousMap.congr_simp
- map_continuousAt
- ContinuousMap.coe_injective'
- CompactlySupportedContinuousMapClass.of_compactSpace
- map_continuousWithinAt
- MeasureTheory.ProbabilityMeasure.continuous_integral_continuousMap
- Bundle.Trivialization.pullback_target
- FiberBundle.pullback_trivializationAt'
- ContinuousMonoidHom.coe_coe
- ContinuousAddMonoidHom.toContinuousMap_toContinuousAddMonoidHom
- FiberBundle.pullback_trivializationAtlas'
- ContinuousMap.coe_apply
- CompactlySupportedContinuousMap.instSMulOfContinuousSMulOfContinuousMapClass
- ContinuousMonoidHom.toContinuousMonoidHom.congr_simp
- Bundle.Trivialization.pullback_symm_apply_proj
- ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass
- ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom
- ContinuousAddMonoidHom.toAddMonoidHom_toContinuousAddMonoidHom
- Bundle.Trivialization.pullback_apply
- ContinuousMap.coe_coe
- MeasureTheory.ProbabilityMeasure.continuous_lintegral_continuousMap
- ContinuousAddMonoidHom.ofClass
- MeasureTheory.FiniteMeasure.continuous_integral_continuousMap
- Bundle.Trivialization.pullback_symm_apply_snd
- Bundle.Trivialization.pullback_baseSet
- FiberBundle.pullback
- ContinuousMonoidHom.ofClass
- ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom
- CompactlySupportedContinuousMap.smulc_apply
- ContinuousMapClass.toCocompactMapClass_of_norm
- instCoeTCContinuousMap
- instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass
- Bundle.Trivialization.pullback_linear
- MeasureTheory.FiniteMeasure.continuous_lintegral_continuousMap
- ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass
- ContinuousAddMonoidHom.coe_coe
- Bundle.Trivialization.pullback_source
- VectorBundle.pullback
- ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact
- CompactlySupportedContinuousMap.coe_smulc
Ancestors0
No ancestors.