Structures · Topology
ContinuousDiv
A typeclass saying that p : G × G ↦ p.1 / p.2 is a continuous function. This property
automatically holds for topological groups. Lemmas using this class have primes.
The unprimed version is for GroupWithZero.
- Defined in
- Mathlib.Topology.Algebra.Group.Defs
- Shape
- One type argument · adds continuous_div'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- SeparationQuotient
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- Filter.Tendsto.div'
- ContinuousDiv.continuous_div'
- MeasureTheory.StronglyMeasurable.div'
- Continuous.fun_div'
- Filter.Tendsto.div_const'
- ContinuousWithinAt.div'
- ContinuousAt.fun_div'
- MeasureTheory.IsStronglyProgressive.div'
- ContinuousOn.div'
- Continuous.div'
- Filter.Tendsto.const_div'
- ContinuousAt.div'
- ContinuousMap.div_comp
- ContinuousMap.div_apply
- IsUniformGroup.of_compactSpace
- ContinuousWithinAt.fun_div'
- ContinuousMap.coe_div
- ContinuousMap.curry_div_apply
- continuous_div_right'
- MeasureTheory.StronglyMeasurable.fun_div'
- Filter.tendsto_div_const_iff
- Filter.tendsto_div_const_iff'
- MeasureTheory.StronglyAdapted.div'
- SeparationQuotient.instContinuousDiv
- SeparationQuotient.instDiv
- SeparationQuotient.mk_div
- ContinuousMap.instDivOfContinuousDiv
- MeasureTheory.ProgMeasurable.div'
- continuous_div_left'
- ContinuousOn.fun_div'
Ancestors0
No ancestors.