nonempty_of_finiteDimensionalOrder

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#LTSeries.nonempty_of_finiteDimensionalOrder

← MathLib Explorer

English

Let α be a type with FiniteDimensionalOrder. Then α is nonempty.

Русский

Пусть α обладает конечномерным порядком. Тогда α непуст.

LaTeX

$$$\forall \alpha\, (\text{FiniteDimensionalOrder }\alpha) \Rightarrow \exists a:\alpha$$$

Lean4

theorem nonempty_of_finiteDimensionalOrder [FiniteDimensionalOrder α] : Nonempty α :=
  by
  obtain ⟨p, _⟩ := (SetRel.finiteDimensional_iff _).mp ‹_›
  exact ⟨p 0⟩

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

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

Разделы

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

Аффилиация

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