source_preimage_target

Mathlib.Topology.OpenPartialHomeomorph

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

English

The source space is contained in the preimage of the target under the forward map.

Русский

Область определения содержится в предобразе цели относительно прямого отображения.

LaTeX

$$$e$.source \subseteq e^{-1}(e.target)$$$

Lean4

theorem source_preimage_target : e.source ⊆ e ⁻¹' e.target :=
  e.mapsTo

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

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

Разделы

Аффилиация

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