Theorems · Definition · Lie groups

ClosedAddSubgroup.casesOn

{G : Type u} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      {motive : ClosedAddSubgroup G → Sort u_1} →
        (t : ClosedAddSubgroup G) →
          ((toAddSubgroup : AddSubgroup G) →
              (isClosed' : IsClosed toAddSubgroup.carrier) →
                motive { toAddSubgroup := toAddSubgroup, 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

AddGroupTopologicalSpace