trans_source''

Mathlib.Logic.Equiv.PartialEquiv

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

English

The domain of e trans e' equals e.symm '' (e.target ∩ e'.source).

Русский

Область определения e trans e' равна e.symm '' (e.target ∩ e'.source).

LaTeX

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

Lean4

theorem trans_source'' : (e.trans e').source = e.symm '' (e.target ∩ e'.source) := by
  rw [e.trans_source', e.symm_image_target_inter_eq]

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

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

Разделы

Аффилиация

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