instFintypeIci — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance instFintypeIci : Fintype (Ici a) :=
  .ofFinset (Finset.Ici a) fun _ => Finset.mem_Ici

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