instFintypeIic — Mathlib

English

Let α be a preorder with a bottom element and locally finite order. Then the interval [−∞, b] is finite for any b ∈ α.

Русский

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

LaTeX

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

Lean4

instance instFintypeIic : Fintype (Iic b) :=
  .ofFinset (Finset.Iic b) fun _ => Finset.mem_Iic

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