t0Space

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#Topology.IsEmbedding.t0Space

← MathLib Explorer

English

If f is an embedding, then the domain X is T0 provided the codomain Y is T0.

Русский

Если f — вложение, то X — T0 при условии, что Y — T0.

LaTeX

$$$t0Space(Top) \text{ from } hf : IsEmbedding(f) ⇒ T0Space(X).$$$

Lean4

protected theorem t0Space [TopologicalSpace Y] [T0Space Y] {f : X → Y} (hf : IsEmbedding f) : T0Space X :=
  t0Space_of_injective_of_continuous hf.injective hf.continuous

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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