Theorems · Definition · global analysis

ChartedSpace.LiftPropOn

{H : Type u_1} →
  {M : Type u_2} →
    {H' : Type u_3} →
      {M' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [ChartedSpace H M] →
              [inst : TopologicalSpace H'] →
                [inst_2 : TopologicalSpace M'] →
                  [ChartedSpace H' M'] → ((H → H') → Set H → H → Prop) → (M → M') → Set M → Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of functions on sets in a charted space, by requiring that it holds around each point of the set, in the preferred charts.

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

16 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceTopologicalSpaceChartedSpace