English
Left invariance under local invariants with open partial homeomorphs.
Русский
Левая инвариантность при локальных инвариантах с открытыми частичными гомоморфами.
LaTeX
$$$left_invariance$ with openPartialHomeomorphs$$
Lean4
theorem left_invariance {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'} (he' : e' ∈ G')
(hfs : ContinuousWithinAt f s x) (hxe' : f x ∈ e'.source) : P (e' ∘ f) s x ↔ P f s x :=
by
have h2f := hfs.preimage_mem_nhdsWithin (e'.open_source.mem_nhds hxe')
have h3f :=
((e'.continuousAt hxe').comp_continuousWithinAt hfs).preimage_mem_nhdsWithin <|
e'.symm.open_source.mem_nhds <| e'.mapsTo hxe'
constructor
· intro h
rw [hG.is_local_nhds h3f] at h
have h2 := hG.left_invariance' (G'.symm he') inter_subset_right (e'.mapsTo hxe') h
rw [← hG.is_local_nhds h3f] at h2
refine hG.congr_nhdsWithin ?_ (e'.left_inv hxe') h2
exact eventually_of_mem h2f fun x' ↦ e'.left_inv
· simp_rw [hG.is_local_nhds h2f]
exact hG.left_invariance' he' inter_subset_right hxe'
