image_eq_target_inter_inv_preimage

Mathlib.Topology.OpenPartialHomeomorph

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

← MathLib Explorer

English

For s ⊆ e.source, the image of s under e equals e.target ∩ e^{-1}(s).

Русский

Для s ⊆ e.source образ множества s под e равен e.target ∩ e^{-1}(s).

LaTeX

$$$e''s = e.target \cap e^{-1}(s)$$$

Lean4

theorem image_eq_target_inter_inv_preimage {s : Set X} (h : s ⊆ e.source) : e '' s = e.target ∩ e.symm ⁻¹' s :=
  e.toPartialEquiv.image_eq_target_inter_inv_preimage h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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