finite_Ioi — Mathlib

English

Let α be a preorder with a top element and locally finite order. Then the interval (a, ∞) is finite for every a.

Русский

Пусть α — предпорядок с верхней границей и локально конечный порядок. Тогда для каждого a множество (a, ∞) конечно.

LaTeX

$$$\forall a \in \alpha, \lvert \{ x \in \alpha \mid a < x \} \rvert < \infty$$$

Lean4

theorem finite_Ioi : (Ioi a).Finite :=
  (Ioi a).toFinite

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