Ioi_disjoint_Iio_same

Mathlib.Order.Interval.Set.Disjoint

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

English

Disjoint (Ioi a) (Iio a).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioi_disjoint_Iio_same : Disjoint (Ioi a) (Iio a) :=
  Ioi_disjoint_Iio_of_le le_rfl

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

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

Разделы

Аффилиация

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