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

Lean4

instance instFintypeIoi : Fintype (Ioi a) :=
  .ofFinset (Finset.Ioi a) fun _ => Finset.mem_Ioi

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