instInfiniteElemIoiOfNoMaxOrder

Mathlib.Order.Interval.Set.Infinite

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

English

In a densely ordered α, for a < b, the set Ico(a, b) is infinite (via Ioo_infinite and subset relation).

Русский

В плотно упорядоченном α при a < b множество Ico(a, b) бесконечно (через Ioo_infinite и вложение).

LaTeX

$$$\forall a,b\ (a

Lean4

instance [NoMaxOrder α] {a : α} : Infinite (Ioi a) :=
  NoMaxOrder.infinite

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

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

Разделы

Аффилиация

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