instInfiniteElemIicOfNoMinOrder

Mathlib.Order.Interval.Set.Infinite

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

English

For a < b with densely ordered α, the set Ioo(a, b) is infinite (as a subtype).

Русский

Для a < b в плотно упорядоченном α множество Ioo(a, b) бесконечно (как подтип).

LaTeX

$$$\forall a,b\ (a

Lean4

instance [NoMinOrder α] {a : α} : Infinite (Iic a) :=
  NoMinOrder.infinite

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

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

Разделы

Аффилиация

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