liftPropWithinAt_indep_chart_source

English

If a germ property P is invariant under the source changes, lifting through source charts remains equivalent.

Русский

Если свойство P инвариантно при изменении источника, то переход через другой источник сохраняет эквивалентность.

LaTeX

$$$P (f \circ g \circ e^{-1}) (s) (x) \iff P (f' \circ g \circ e'^{-1}) (s)(x).$$$

Lean4

/-- A version of `liftPropWithinAt_indep_chart`, only for the source. -/
theorem liftPropWithinAt_indep_chart_source [HasGroupoid M G] (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source) :
    LiftPropWithinAt P g s x ↔ LiftPropWithinAt P (g ∘ e.symm) (e.symm ⁻¹' s) (e x) :=
  by
  rw [liftPropWithinAt_self_source, liftPropWithinAt_iff',
    e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe, e.symm_symm]
  refine and_congr Iff.rfl ?_
  rw [Function.comp_apply, e.left_inv xe, ← Function.comp_assoc,
    hG.liftPropWithinAt_indep_chart_source_aux (chartAt _ (g x) ∘ g) (chart_mem_maximalAtlas G x) (mem_chart_source _ x)
      he xe,
    Function.comp_assoc]

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