H : Type u_1
M : Type ?u.2794
H' : Type u_2
M' : Type ?u.2800
X : Type ?u.2803
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s✝ t u : Set H
x✝ : H
hG : LocalInvariantProp G G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x | f x = g x}) x ↔ P g (s ∩ {x | f x = g x}) x
H : Type u_1
M : Type ?u.2794
H' : Type u_2
M' : Type ?u.2800
X : Type ?u.2803
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s✝ t u : Set H
x✝ : H
hG : LocalInvariantProp G G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f s x ↔ P g s x
simp_rw [hG.is_local_nhds h1]
no goals
H : Type u_1
M : Type ?u.2794
H' : Type u_2
M' : Type ?u.2800
X : Type ?u.2803
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s✝ t u : Set H
x✝ : H
hG : LocalInvariantProp G G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f (s ∩ {x | f x = g x}) x ↔ P g (s ∩ {x | f x = g x}) x
exact ⟨hG.congr_of_forall (fun y hy ↦ hy.2) h2, hG.congr_of_forall (fun y hy ↦ hy.2.symm) h2.symm⟩