Structures · Topology
IsTopologicalAddTorsor
A topological torsor over a topological additive group is a torsor where +ᵥ and -ᵥ are
continuous.
- Defined in
- Mathlib.Topology.Algebra.Group.Torsor
- Shape
- One type argument · adds continuous_vsub
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Subtype
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by95
- ContinuousAffineMap.contLinear
- Homeomorph.vaddConst
- AffineMap.lineMap_continuous
- ContinuousAffineMap.decompEquiv
- ContinuousAffineEquiv.pointReflection
- ContinuousAffineMap.decompAffineEquiv
- AffineMap.lineMap_continuous_uncurry
- Filter.Tendsto.vsub
- Homeomorph.vaddConst_symm_apply
- Homeomorph.constVSub
- ContinuousAffineEquiv.vaddConst
- ContinuousAffineEquiv.constVSub
- Continuous.vsub
- Homeomorph.pointReflection
- ContinuousAffineMap.lineMap_apply'
- Filter.Tendsto.lineMap
- AffineMap.isOpenMap_linear_iff
- AffineMap.continuous_linear_iff
- ContinuousAffineMap.map_vadd
- AffineMap.homothety_continuous
- ContinuousAffineMap.contLinear_map_vsub
- Homeomorph.vaddConst_apply
- IsTopologicalAddTorsor.continuous_vsub
- ContinuousAt.vsub
- ContinuousAffineMap.decompEquiv_symm_contLinear
- AffineMap.homothety_isOpenMap
- ContinuousAffineMap.coe_linear_eq_coe_contLinear
- ContinuousAffineMap.comp_contLinear
- AffineSpace.asymptoticNhds_bind_nhds
- AffineSubspace.isClosed_direction_iff
- eventually_homothety_mem_of_mem_interior
- ContinuousAffineMap.coe_mk_contLinear_eq_linear
- ContinuousAffineMap.coe_contLinear_eq_linear
- Affine.Simplex.isCompact_closedInterior
- IsTopologicalAddTorsor.to_isTopologicalAddGroup
- ContinuousWithinAt.vsub
- asymptoticCone_closure
- Filter.Tendsto.midpoint
- Homeomorph.constVSub_symm_apply
- eventually_homothety_image_subset_of_finite_subset_interior
- ContinuousAt.lineMap
- ContinuousAffineEquiv.pointReflection_symm
- ContinuousAffineMap.linear_decompAffineEquiv
- ContinuousAffineMap.zero_contLinear
- Affine.Simplex.isClosed_closedInterior
- ContinuousAffineEquiv.pointReflection_involutive
- ContinuousAffineMap.vsub_toAffineMap
- AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection
- ContinuousAffineMap.decompAffineEquiv_symm_contLinear
- ContinuousAffineMap.neg_contLinear