Theorems · Theorem · global analysis

StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2

∀ {H : Type u_1} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H']
  [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ (g : H → M') {x : H} {s : Set H},
      f ∈ StructureGroupoid.maximalAtlas M' G' →
        g x ∈ f.source → ContinuousWithinAt g s x → (P (↑(chartAt H' (g x)) ∘ g) s x ↔ P (↑f ∘ g) s x)

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpace