trans_target''

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.trans_target''

English

The target of e trans e' equals e' '' (e'.source ∩ e'.target) as a set image.

Русский

Цель композиции e trans e' равна e' '' (e'.source ∩ e'.target).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru