Theorems · Definition · Lie groups

IsTopologicalTorsor.recOn

{V : Type u_1} →
  [inst : Group V] →
    [inst_1 : TopologicalSpace V] →
      {P : Type u_2} →
        [inst_2 : Torsor V P] →
          [inst_3 : TopologicalSpace P] →
            {motive : IsTopologicalTorsor P → Sort u} →
              (t : IsTopologicalTorsor P) →
                ([toContinuousSMul : ContinuousSMul V P] →
                    (continuous_sdiv : Continuous fun x => x.1 /ₛ x.2) → motive ⋯) →
                  motive t

Defined in

Mathlib.Topology.Algebra.Group.Torsor

Cited by

0 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceTorsorTopologicalSpace