Theorems · Definition · Lie groups

ClosedSubgroup.recOn

{G : Type u} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      {motive : ClosedSubgroup G → Sort u_1} →
        (t : ClosedSubgroup G) →
          ((toSubgroup : Subgroup G) →
              (isClosed' : IsClosed toSubgroup.carrier) → motive { toSubgroup := toSubgroup, isClosed' := isClosed' }) →
            motive t

Defined in

Mathlib.Topology.Algebra.Group.ClosedSubgroup

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

GroupTopologicalSpace