nonempty_of_infiniteDimensional

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.nonempty_of_infiniteDimensional

← MathLib Explorer

English

If a relation on α is infinite dimensional, then α is nonempty.

Русский

Если отношение на α бесконечно размерно, то α непусто.

LaTeX

$$$[r.InfiniteDimensional] \\Rightarrow \\operatorname{Nonempty}(\\alpha)$$$

Lean4

/-- If a relation on `α` is infinite dimensional, then `α` is nonempty. -/
theorem nonempty_of_infiniteDimensional [r.InfiniteDimensional] : Nonempty α :=
  ⟨RelSeries.withLength r 0 0⟩

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

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

Разделы

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

Аффилиация

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