image_trans_source — Mathlib

English

The target of the composed map can also be described as the image of the second target under the inverse of the second map, intersected with the first target.

Русский

Целевой предел составного отображения может быть описан как образ второй целевой области под обратным отображением второго отображения, пересечённый с первой целевой областью.

LaTeX

$$$ (e.trans e').target = e'.target \\cap e'.symm^{-1} e.target $$$

Lean4

theorem image_trans_source : e '' (e.trans e').source = e.target ∩ e'.source :=
  PartialEquiv.image_trans_source e.toPartialEquiv e'.toPartialEquiv

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