Theorems · Definition · Lie groups

OpenSubgroup.casesOn

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

Defined in

Mathlib.Topology.Algebra.OpenSubgroup

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

GroupTopologicalSpace