Structures · Topology
ContinuousSub
A typeclass saying that p : G × G ↦ p.1 - p.2 is a continuous function. This property
automatically holds for topological additive groups but it also holds, e.g., for ℝ≥0.
- Defined in
- Mathlib.Topology.Algebra.Group.Defs
- Shape
- One type argument · adds continuous_sub
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- SeparationQuotient
- NNReal
- NNRat
How is a type an instance?
Loading the hierarchy index…
Assumed by57
- Filter.Tendsto.sub
- Continuous.fun_sub
- Continuous.sub
- ContinuousOn.sub
- ContinuousAt.fun_sub
- MeasureTheory.StronglyMeasurable.sub
- ContinuousOn.fun_sub
- Filter.Tendsto.const_sub
- Filter.Tendsto.sub_const
- Submodule.IsTopCompl.symm
- ContinuousWithinAt.sub
- ContinuousAt.sub
- ContinuousSub.continuous_sub
- continuous_sub_right
- continuous_sub_left
- Submodule.IsTopCompl.isClosed
- Filter.tendsto_sub_const_iff
- Submodule.projectionL_add_projectionL_eq_self
- MeasureTheory.StronglyAdapted.sub
- ContinuousLinearMap.isOpenMap_of_ne_zero
- Submodule.projectionL_eq_self_sub_projectionL
- liminf_const_sub
- limsup_const_sub
- Submodule.isTopCompl_comm
- MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat
- MeasureTheory.AEFinStronglyMeasurable.sub
- continuous_skewAdjointPart
- MeasureTheory.FinStronglyMeasurable.sub
- ContinuousMap.AlgHom.closure_ker_inter
- skewAdjointPartL
- MeasureTheory.IsStronglyProgressive.sub
- Submodule.ClosedComplemented.isClosed
- limsup_sub_const
- ContinuousLinearMap.closedComplemented_ker_of_rightInverse
- ContinuousMap.curry_sub_apply
- ContinuousMapZero.coe_sub
- ContinuousWithinAt.fun_sub
- ContinuousMap.instSubOfContinuousSub
- BoundedContinuousFunction.instSub
- ContinuousMap.coe_sub
- MeasureTheory.StronglyMeasurable.fun_sub
- liminf_sub_const
- SeparationQuotient.instContinuousSub
- Continuous.convolution_integrand_fst
- ContinuousMap.sub_apply
- ContinuousMapZero.instSub
- MeasureTheory.ProgMeasurable.sub
- IsUniformAddGroup.of_compactSpace
- BoundedContinuousFunction.sub_apply
- skewAdjointPartL_apply_coe
Ancestors0
No ancestors.