Ioc_infinite

Mathlib.Order.Interval.Set.Infinite

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

English

In a densely ordered α, for a < b, the interval Ioc(a, b) has infinitely many elements (as a subtype).

Русский

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

LaTeX

$$$\forall a,b\ (a

Lean4

theorem Ioc_infinite : (Ioc a b).Infinite :=
  (Ioo_infinite h).mono Ioo_subset_Ioc_self

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

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

Разделы

Аффилиация

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