Theorems · Definition · category theory

StructureGroupoid.LocalInvariantProp.localPredicate

{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] →
                  [ChartedSpace H M] →
                    (M' : Type u) →
                      [inst_4 : TopologicalSpace M'] →
                        [ChartedSpace H' M'] → G.LocalInvariantProp G' P → TopCat.LocalPredicate fun x => M'

Let P be a LocalInvariantProp for functions between spaces with the groupoids G, G' and let M, M' be charted spaces modelled on the model spaces of those groupoids. Then there is an induced LocalPredicate on the functions from M to M', given by LiftProp P.

Defined in

Mathlib.Geometry.Manifold.Sheaf.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace