liftPropWithinAt_indep_chart_target_aux

English

Equivalence of Germ property P for representations with different target charts in the presence of invariance under the structure groupoid and continuity assumptions on g.

Русский

Эквивалентность свойства жерма P для различных целевых чартов при условии инвариантности и непрерывности.

LaTeX

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

Lean4

theorem liftPropWithinAt_indep_chart_target_aux {g : X → M'} {e : OpenPartialHomeomorph X H} {x : X} {s : Set X}
    (xe : x ∈ e.source) (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 ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (f' ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) :=
  by
  rw [← e.left_inv xe] at xf xf' hgs
  refine hG.liftPropWithinAt_indep_chart_target_aux2 (g ∘ e.symm) hf xf hf' xf' ?_
  exact hgs.comp (e.symm.continuousAt <| e.mapsTo xe).continuousWithinAt Subset.rfl

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