inv_image_trans_target — Mathlib

English

The inverse image under e'.symm of the target of e trans e' is equal to Dom(e') ∩ Ran(e).

Русский

Обратное изображение под e'.symm целевой части e trans e' равно Dom(e') ∩ Ran(e).

LaTeX

$$$e'.\mathrm{symm} '' (e.\mathrm{trans} e').\mathrm{target} = e'.\mathrm{source} \cap e.\mathrm{target}$$$

Lean4

theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩ e.target :=
  image_trans_source e'.symm e.symm

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