image_trans_source — Mathlib

English

The image of the domain of e under e is equal to e.target ∩ e'.source when composing with e'.

Русский

Образ области определения e под действием e совпадает с e.target ∩ e'.source при композиции.

LaTeX

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

Lean4

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

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