preimage_symm

Mathlib.Topology.Homeomorph.Defs

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

English

For any subset S of Y, the image of its preimage under h equals S.

Русский

Для любого подмножества S ⊆ Y образ его предобраза под h равен S.

LaTeX

$$$h[\,h^{-1}(S)\] = S\\quad (S\\subseteq Y)$$$

Lean4

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

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

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

Разделы

Аффилиация

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