symm_mapsTo

Mathlib.Logic.Equiv.PartialEquiv

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

English

MapsTo holds for the inverse: MapsTo e.symm.toFun (e.target ∩ t) (e.source ∩ s).

Русский

У обратного сохраняется отображение: MapsTo e.symm.toFun (e.target ∩ t) (e.source ∩ s).

LaTeX

$$MapsTo e.symm.toFun (e.target ∩ t) (e.source ∩ s)$$

Lean4

theorem symm_mapsTo (h : e.IsImage s t) : MapsTo e.symm (e.target ∩ t) (e.source ∩ s) :=
  h.symm.mapsTo

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

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

Разделы

Аффилиация

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