discreteTopology

Mathlib.Topology.Homeomorph.Defs

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

English

A homeomorphism preserves openness of sets via preimage.

Русский

Гомеоморфизм сохраняет открытость через предобраз.

LaTeX

$$IsOpen(h^{-1}[S]) \\iff IsOpen(S)$$

Lean4

protected theorem discreteTopology [DiscreteTopology X] (h : X ≃ₜ Y) : DiscreteTopology Y :=
  h.symm.isEmbedding.discreteTopology

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

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

Разделы

Аффилиация

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