isSeparatedMap

Mathlib.Topology.SeparatedMap

URI: https://scilib.ai/kg/mathlib#T2Space.isSeparatedMap

English

If X is Hausdorff, then any map f: X→Y is separated.

Русский

Если X хаусдорфово, то любая карта f: X→Y разделима.

LaTeX

$$$$[\\text{T2Space}(X)] \\Rightarrow \\operatorname{IsSeparatedMap}(f) \\text{ for any } f:X\\to Y.$$$$

Lean4

theorem isSeparatedMap [T2Space X] (f : X → Y) : IsSeparatedMap f := fun _ _ _ ↦ t2_separation

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

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

Разделы

Аффилиация

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