map_source

Mathlib.Logic.Equiv.PartialEquiv

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

English

If y ∈ e.target, then e.symm y ∈ e.source.

Русский

Если y принадлежит целевой области, то e.symm y принадлежит области источника.

LaTeX

$$$\forall y\in e.\mathrm{target},\ e^{-1}(y) \in e.\mathrm{source}$$$

Lean4

@[simp, mfld_simps]
theorem map_source {x : α} (h : x ∈ e.source) : e x ∈ e.target :=
  e.map_source' h

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

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

Разделы

Аффилиация

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