nodup_Ico

Mathlib.Order.Interval.Multiset

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

English

(Ico a b).Nodup.

Русский

У Ico(a,b) нет повторов.

LaTeX

$$$(\mathrm{Ico}(a,b)).\mathrm{Nodup}$$$

Lean4

theorem nodup_Ico : (Ico a b).Nodup :=
  Finset.nodup _

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

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

Разделы

Аффилиация

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