symm_mapsTo

Mathlib.Topology.OpenPartialHomeomorph

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

English

The inverse map e.symm maps e.target into e.source.

Русский

Обратное отображение e.symm отображает e.target в e.source.

LaTeX

$$$ \mathrm{MapsTo}(e.symm, e.target, e.source).$$$

Lean4

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

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

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

Разделы

Аффилиация

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