finite_Ici — 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 \le x \} \rvert < \infty$$$

Lean4

theorem finite_Ici : (Ici a).Finite :=
  (Ici a).toFinite

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