Theorems · Inductive type · Lie groups

IsTopologicalTorsor

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

A topological torsor over a topological group is a torsor where • and /ₛ are continuous.

Defined in

Mathlib.Topology.Algebra.Group.Torsor

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

GroupTopologicalSpaceTorsorTopologicalSpace