Theorems · Inductive type · Lie groups

IsTopologicalAddTorsor

{V : Type u_1} →
  [inst : AddGroup V] → [TopologicalSpace V] → (P : Type u_2) → [AddTorsor V P] → [TopologicalSpace P] → Prop

A topological torsor over a topological additive group is a torsor where +ᵥ and -ᵥ are continuous.

Defined in

Mathlib.Topology.Algebra.Group.Torsor

Cited by

80 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddGroupTopologicalSpaceAddTorsorTopologicalSpace