t1Space

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.t1Space

← MathLib Explorer

English

Every manifold is a T1 space.

Русский

Каждое многообразие является пространством T1.

LaTeX

$$T1Space M$$

Lean4

/-- Every manifold is a Fréchet space (T1 space) -- regardless of whether it is
Hausdorff. -/
protected theorem t1Space (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : T1Space M :=
  by
  have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space
  exact ChartedSpace.t1Space H M

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

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

Разделы

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

Аффилиация

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