Theorems · Definition · Lie groups

OpenSubgroup.mk.noConfusion

{G : Type u_1} →
  {inst : Group G} →
    {inst_1 : TopologicalSpace G} →
      {P : Sort u} →
        {toSubgroup : Subgroup G} →
          {isOpen' : IsOpen toSubgroup.carrier} →
            {toSubgroup' : Subgroup G} →
              {isOpen'' : IsOpen toSubgroup'.carrier} →
                { toSubgroup := toSubgroup, isOpen' := isOpen' } = { toSubgroup := toSubgroup', isOpen' := isOpen'' } →
                  (toSubgroup ≍ toSubgroup' → P) → P

Defined in

Mathlib.Topology.Algebra.OpenSubgroup

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms