extend_preimage_inter_eq — Mathlib

English

The image under the extended chart of the intersection of the sources equals the source of the translated extended chart; this ties together the interaction of sources under extension.

Русский

Образ под расширенной картой пересечения источников равен источнику преобразованной расширенной карты.

LaTeX

$$$f.extend I '' (f.source \\cap f'.source) = ((f.extend I)^{-1} \\circ f'.extend I).source$$$

Lean4

/-- Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to
bring it into a convenient form to apply derivative lemmas. -/
theorem extend_preimage_inter_eq :
    (f.extend I).symm ⁻¹' (s ∩ t) ∩ range I = (f.extend I).symm ⁻¹' s ∩ range I ∩ (f.extend I).symm ⁻¹' t := by
  mfld_set_tac

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