source_subset_preimage_target

Mathlib.Logic.Equiv.PartialEquiv

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

English

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

Русский

Источник содержится в предобразе целевого множества под отображением e.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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