Ico_eq_zero_iff

Mathlib.Order.Interval.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.Ico_eq_zero_iff

English

Ico(a,b) is empty if and only if not a < b.

Русский

Ico(a,b) пусто тогда и только тогда, когда не выполняется a < b.

LaTeX

$$$\mathrm{Ico}(a,b) = 0 \iff \neg (a < b)$$$

Lean4

@[simp]
theorem Ico_eq_zero_iff : Ico a b = 0 ↔ ¬a < b := by rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]

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

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

Разделы

Аффилиация

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