Theorems · Theorem · global analysis

StructureGroupoid.LocalInvariantProp.left_invariance

∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'},
      e' ∈ G' → ContinuousWithinAt f s x → f x ∈ e'.source → (P (↑e' ∘ f) s x ↔ P f s x)

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace