infinite

Mathlib.Order.Interval.Set.Infinite

URI: https://scilib.ai/kg/mathlib#Set.Ioc.infinite

English

For an a < b in a densely ordered α, the set Ioc(a, b) is infinite.

Русский

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

LaTeX

$$$\forall a,b\ (a

Lean4

theorem infinite : Infinite (Ioc a b) :=
  infinite_coe_iff.2 <| Ioc_infinite h

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

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

Разделы

Аффилиация

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