Theorems · Theorem · Lie groups

OpenSubgroup.mk.injEq

∀ {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

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

GroupTopologicalSpace