finite_Iio

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Set.finite_Iio

English

Let α be a preorder with a bottom element and locally finite order. Then the interval (−∞, b) is finite.

Русский

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

LaTeX

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

Lean4

theorem finite_Iio : (Iio b).Finite :=
  (Iio b).toFinite

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru