Theorems · Inductive type · global analysis

ChartedSpace.LiftPropWithinAt

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

Given a property of germs of functions and sets in the model space, then one defines a corresponding property in a charted space, by requiring that it holds at the preferred chart at this point. (When the property is local and invariant, it will in fact hold using any chart, see liftPropWithinAt_indep_chart). We require continuity in the lifted property, as otherwise one single chart might fail to capture the behavior of the function.

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

37 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceTopologicalSpaceChartedSpace