not_finiteDimensionalOrder_iff — Mathlib

English

For a nonempty preorder α, the property of not being finite-dimensional is equivalent to being infinite-dimensional.

Русский

Для ненулевого предпорядка α свойство «не конечная размерность» эквивалентно «бесконечная размерность».

LaTeX

$$$\\neg FiniteDimensionalOrder(\\alpha) \\iff InfiniteDimensionalOrder(\\alpha)$$$

Lean4

theorem not_finiteDimensionalOrder_iff [Preorder α] [Nonempty α] :
    ¬FiniteDimensionalOrder α ↔ InfiniteDimensionalOrder α :=
  SetRel.not_finiteDimensional_iff

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