Iio_infinite

Mathlib.Order.Interval.Set.Infinite

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

English

If NoMinOrder holds, then (Iio a) is infinite for any a.

Русский

Если выполняется NoMinOrder, то (Iio a) бесконечен для любого a.

LaTeX

$$$\forall a\; (\mathrm{Iio}(a)).\text{Infinite}$$$

Lean4

theorem Iio_infinite [NoMinOrder α] (a : α) : (Iio a).Infinite :=
  infinite_coe_iff.1 inferInstance

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

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

Разделы

Аффилиация

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