image_symm

Mathlib.Topology.Homeomorph.Defs

URI: https://scilib.ai/kg/mathlib#Homeomorph.image_symm

English

For a homeomorphism h, the image of a set under h^{-1} equals the preimage of that set under h.

Русский

Для гомеоморфизма h образ множества под h^{-1} равен предобразу этого множества под h.

LaTeX

$$For all S \\subseteq Y, h^{-1}[S] = { h^{-1}(y) : y \\in S }$$

Lean4

theorem image_symm (h : X ≃ₜ Y) : image h.symm = preimage h :=
  funext h.symm.toEquiv.image_eq_preimage

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

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

Разделы

Аффилиация

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