Theorems · Theorem · global analysis

Structomorph.mk.sizeOf_spec

∀ {H : Type u} [inst : TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6}
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H M] [inst_4 : ChartedSpace H M']
  [inst_5 : SizeOf H] [inst_6 : SizeOf M] [inst_7 : SizeOf M'] (toHomeomorph : M ≃ₜ M')
  (mem_groupoid :
    ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
      c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G),
  sizeOf { toHomeomorph := toHomeomorph, mem_groupoid := mem_groupoid } = 1 + sizeOf toHomeomorph

Defined in

Mathlib.Geometry.Manifold.HasGroupoid

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceChartedSpaceSizeOfSizeOfSizeOf