Theorems · Definition · global analysis

ChartedSpace.LiftPropAt

{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') → M → Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of a function at a point in a charted space, by requiring that it holds in the preferred chart.

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

14 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceTopologicalSpaceChartedSpace