Ico_self

Mathlib.Order.Interval.Set.Basic

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

English

The interval Ico(a,a) is empty.

Русский

Интервал Ico(a,a) пуст.

LaTeX

$$$ \mathrm{Ico}(a,a) = \emptyset $$$

Lean4

theorem Ico_self (a : α) : Ico a a = ∅ :=
  Ico_eq_empty <| lt_irrefl _

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

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

Разделы

Аффилиация

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