image_eq_preimage

Mathlib.Topology.Homeomorph.Defs

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

English

A homeomorphism induces the target topology from the source topology.

Русский

Гомеоморфизм индуцирует топологию целевого пространства из топологии исходного.

LaTeX

$$IsInducing(h)$$

Lean4

theorem image_eq_preimage (h : X ≃ₜ Y) (s : Set X) : h '' s = h.symm ⁻¹' s :=
  h.toEquiv.image_eq_preimage s

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

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

Разделы

Аффилиация

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