Theorems · Theorem · Lie groups

ClosedAddSubgroup.mk.sizeOf_spec

∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G] (toAddSubgroup : AddSubgroup G)
  (isClosed' : IsClosed toAddSubgroup.carrier),
  sizeOf { toAddSubgroup := toAddSubgroup, isClosed' := isClosed' } = 1 + sizeOf toAddSubgroup + sizeOf isClosed'

Defined in

Mathlib.Topology.Algebra.Group.ClosedSubgroup

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

AddGroupTopologicalSpaceSizeOf