trans_target' — Mathlib

English

The target of the composition equals the intersection of the second target with the preimage of the first target under the inverse of the second map.

Русский

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

LaTeX

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

Lean4

theorem trans_target' : (e.trans e').target = e'.target ∩ e'.symm ⁻¹' (e'.source ∩ e.target) :=
  trans_source' e'.symm e.symm

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