image_compl

Mathlib.Topology.Homeomorph.Defs

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

English

The topology on Y is the topology induced by h from X.

Русский

Топология Y равно топологии, индуцированной через h из X.

LaTeX

$$$\\mathcal{T}_Y = \\mathcal{T}_X^{h\\text{-induced}}$$$

Lean4

theorem image_compl (h : X ≃ₜ Y) (s : Set X) : h '' (sᶜ) = (h '' s)ᶜ :=
  h.toEquiv.image_compl s

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

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

Разделы

Аффилиация

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