extend_image_source_inter — Mathlib

English

The image under the extended chart of the intersection of sources corresponds to the source of the composed extended charts; this ties together the image of intersections under extension.

Русский

Изображение пересечения источников под расширенной картой соответствует источнику композиции расширенных карт.

LaTeX

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

Lean4

theorem extend_image_source_inter : f.extend I '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ f'.extend I).source :=
  by simp_rw [f.extend_coord_change_source, f.extend_coe, image_comp I f, trans_source'', symm_symm, symm_target]

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