Theorems · Theorem · Lie groups

OpenSubgroup.mk.inj

∀ {G : Type u_1} {inst : Group G} {inst_1 : TopologicalSpace G} {toSubgroup : Subgroup G}
  {isOpen' : IsOpen toSubgroup.carrier} {toSubgroup_1 : Subgroup G} {isOpen'_1 : IsOpen toSubgroup_1.carrier},
  { toSubgroup := toSubgroup, isOpen' := isOpen' } = { toSubgroup := toSubgroup_1, isOpen' := isOpen'_1 } →
    toSubgroup = toSubgroup_1

Defined in

Mathlib.Topology.Algebra.OpenSubgroup

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms