Theorems · Theorem · Lie groups

ClosedSubgroup.mk.inj

∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {toSubgroup : Subgroup G}
  {isClosed' : IsClosed toSubgroup.carrier} {toSubgroup_1 : Subgroup G} {isClosed'_1 : IsClosed toSubgroup_1.carrier},
  { toSubgroup := toSubgroup, isClosed' := isClosed' } = { toSubgroup := toSubgroup_1, isClosed' := isClosed'_1 } →
    toSubgroup = toSubgroup_1

Defined in

Mathlib.Topology.Algebra.Group.ClosedSubgroup

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms