∀ {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 g : H → H'}, f =ᶠ[nhds x] g → P g s x → P f s x