Theorems · Theorem · category theory

StructureGroupoid.LocalInvariantProp.section_spec

∀ {H : Type u_1} [inst : TopologicalSpace H] {H' : Type u_2} [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [inst_2 : TopologicalSpace M]
  [inst_3 : ChartedSpace H M] (M' : Type u) [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M']
  (hG : G.LocalInvariantProp G' P) (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
  (f : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).obj.obj U), ChartedSpace.LiftProp P ↑f

Defined in

Mathlib.Geometry.Manifold.Sheaf.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace