mem_symm_trans_source — Mathlib

English

If x lies in the source of e and in the source of e', then e(x) lies in the source of the composed chart e.symm.trans e'.

Русский

Если x принадлежит области определения e и e', то e(x) принадлежит области определения композиции e.symm.trans e'.

LaTeX

$$$ x \\in e.source \\wedge x \\in e'.source \\quad \\Rightarrow \\quad e(x) \\in (e^{-1} \\circ e').source $$$

Lean4

/-- A lemma commonly useful when `e` and `e'` are charts of a manifold. -/
theorem mem_symm_trans_source {e' : PartialEquiv α γ} {x : α} (he : x ∈ e.source) (he' : x ∈ e'.source) :
    e x ∈ (e.symm.trans e').source :=
  ⟨e.mapsTo he, by rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]⟩

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