Iio_disjoint_Ioi_same

Mathlib.Order.Interval.Set.Disjoint

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

English

Disjoint (Iio a) (Ioi a).

Русский

Iio(a) и Ioi(a) не пересекаются.

LaTeX

$$$$ Disjoint (Iio\,a) (Ioi\,a). $$$$

Lean4

@[simp]
theorem Iio_disjoint_Ioi_same : Disjoint (Iio a) (Ioi a) :=
  Iio_disjoint_Ioi_of_le le_rfl

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

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

Разделы

Аффилиация

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