infinite

Mathlib.Topology.Separation.Connected

URI: https://scilib.ai/kg/mathlib#PreconnectedSpace.infinite

← MathLib Explorer

English

If X is a preconnected space and nontrivial and T1, then X is infinite.

Русский

Если X предсоединено, непусто и T1, то X бесконечно.

LaTeX

$$$\text{IsPreconnected}(X) \land \text{Nontrivial}(X) \land \text{T1Space}(X) \Rightarrow \text{Infinite}(X)$$$

Lean4

theorem infinite [PreconnectedSpace X] [Nontrivial X] [T1Space X] : Infinite X :=
  infinite_univ_iff.mp <| isPreconnected_univ.infinite_of_nontrivial nontrivial_univ

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

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

Разделы

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

Аффилиация

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