Structures · Topology
IsTopologicalTorsor
A topological torsor over a topological group is a torsor where • and /ₛ are continuous.
- Defined in
- Mathlib.Topology.Algebra.Group.Torsor
- Shape
- One type argument · adds continuous_sdiv
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- Homeomorph.constSDiv
- Homeomorph.smulConst
- Filter.Tendsto.sdiv
- IsTopologicalTorsor.continuous_sdiv
- ContinuousWithinAt.sdiv
- Continuous.sdiv
- Homeomorph.smulConst_apply
- Homeomorph.constSDiv_apply
- instProperSMul
- instIsTopologicalTorsorProd
- instIsTopologicalTorsorForall
- IsTopologicalTorsor.toContinuousSMul
- IsTopologicalTorsor.to_isTopologicalGroup
- Homeomorph.smulConst_symm_apply
- ContinuousAt.sdiv
- ContinuousOn.sdiv
- Homeomorph.constSDiv_symm_apply