symm_mapsTo

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.symm_mapsTo

English

The inverse map sends the target into the source.

Русский

Обратное отображение переводит целевую область обратно в источник.

LaTeX

$$$\text{MapsTo } e.symm\, e. target\ e. source$$$

Lean4

theorem symm_mapsTo : MapsTo e.symm e.target e.source :=
  e.symm.mapsTo

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

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

Разделы

Аффилиация

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