instFintypeIio — 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 < b \} \rvert < \infty$$$

Lean4

instance instFintypeIio : Fintype (Iio b) :=
  .ofFinset (Finset.Iio b) fun _ => Finset.mem_Iio

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