Theorems · Inductive type · global analysis

StructureGroupoid.LocalInvariantProp

{H : Type u_1} →
  {H' : Type u_3} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace H'] → StructureGroupoid H → StructureGroupoid H' → ((H → H') → Set H → H → Prop) → Prop

Structure recording good behavior of a property of a triple (f, s, x) where f is a function, s a set and x a point. Good behavior here means locality and invariance under given groupoids (both in the source and in the target). Given such a good behavior, the lift of this property to charted spaces admitting these groupoids will inherit the good behavior.

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

64 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace