English
If two source charts e and e' are compatible and parts of the maximal atlas, then P expressed via e and via e' with appropriate preimages are equivalent at x.
Русский
Если два источника совместимы и принадлежат атласу, то P через e и через e' эквивалентны в точке x.
LaTeX
$$$P (f \circ g) \circ e^{-1} \; s \; x \iff P (f' \circ g) \circ e'^{-1} \; s \; x.$$$
Lean4
theorem liftPropWithinAt_indep_chart_source_aux (g : M → H') (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source)
(he' : e' ∈ G.maximalAtlas M) (xe' : x ∈ e'.source) :
P (g ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (g ∘ e'.symm) (e'.symm ⁻¹' s) (e' x) :=
by
rw [← hG.right_invariance (compatible_of_mem_maximalAtlas he he')]
swap; · simp only [xe, xe', mfld_simps]
simp_rw [OpenPartialHomeomorph.trans_apply, e.left_inv xe]
rw [hG.congr_iff]
· refine hG.congr_set ?_
refine (eventually_of_mem ?_ fun y (hy : y ∈ e'.symm ⁻¹' e.source) ↦ ?_).set_eq
· refine (e'.symm.continuousAt <| e'.mapsTo xe').preimage_mem_nhds (e.open_source.mem_nhds ?_)
simp_rw [e'.left_inv xe', xe]
simp_rw [mem_preimage, OpenPartialHomeomorph.coe_trans_symm, OpenPartialHomeomorph.symm_symm, Function.comp_apply,
e.left_inv hy]
· refine ((e'.eventually_nhds' _ xe').mpr <| e.eventually_left_inverse xe).mono fun y hy ↦ ?_
simp only [mfld_simps]
rw [hy]
