not_infiniteDimensionalOrder_iff — Mathlib

English

For a preorder α with a nonempty domain, not infinite-dimensional is equivalent to finite-dimensional.

Русский

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

LaTeX

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

Lean4

theorem not_infiniteDimensionalOrder_iff [Preorder α] [Nonempty α] :
    ¬InfiniteDimensionalOrder α ↔ FiniteDimensionalOrder α :=
  SetRel.not_infiniteDimensional_iff

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