liftPropOn_indep_chart — Mathlib

English

Analogous result for target charts with two representations f and f'.

Русский

Аналогично для целевых чартов f и f'.

LaTeX

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

Lean4

theorem liftPropOn_indep_chart [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ G.maximalAtlas M)
    (hf : f ∈ G'.maximalAtlas M') (h : LiftPropOn P g s) {y : H} (hy : y ∈ e.target ∩ e.symm ⁻¹' (s ∩ g ⁻¹' f.source)) :
    P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) y :=
  by
  convert ((hG.liftPropWithinAt_indep_chart he (e.symm_mapsTo hy.1) hf hy.2.2).1 (h _ hy.2.1)).2
  rw [e.right_inv hy.1]

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