liftPropWithinAt_indep_chart_target_aux2

English

Given g: H → M' and two target charts f, f' with atlas membership, the equivalence of P holds when applying g into the target coordinate representations.

Русский

Дано g: H→M' и два целевых чарта f,f' атласа; эквивалентность P сохраняется под преобразованием через g.

LaTeX

$$$P (f \circ g) \; s \; x \iff P (f' \circ g) \; s \; x.$$$

Lean4

theorem liftPropWithinAt_indep_chart_target_aux2 (g : H → M') {x : H} {s : Set H} (hf : f ∈ G'.maximalAtlas M')
    (xf : g x ∈ f.source) (hf' : f' ∈ G'.maximalAtlas M') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) :
    P (f ∘ g) s x ↔ P (f' ∘ g) s x :=
  by
  have hcont : ContinuousWithinAt (f ∘ g) s x := (f.continuousAt xf).comp_continuousWithinAt hgs
  rw [← hG.left_invariance (compatible_of_mem_maximalAtlas hf hf') hcont (by simp only [xf, xf', mfld_simps])]
  refine hG.congr_iff_nhdsWithin ?_ (by simp only [xf, mfld_simps])
  exact (hgs.eventually <| f.eventually_left_inverse xf).mono fun y ↦ congr_arg f'

Похожие утверждения