trans_source'' — Mathlib

English

The target (codomain) of the composition is the intersection of the second target with the preimage of the first target under the inverse.

Русский

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

LaTeX

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

Lean4

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

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