nonempty_of_finiteDimensional

Mathlib.Order.RelSeries

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

English

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

Русский

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

LaTeX

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

Lean4

theorem nonempty_of_finiteDimensional [r.FiniteDimensional] : Nonempty α :=
  by
  obtain ⟨p, _⟩ := (r.finiteDimensional_iff).mp ‹_›
  exact ⟨p 0⟩

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

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

Разделы

Аффилиация

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