nodup_Icc

Mathlib.Order.Interval.Multiset

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

English

(Icc a b).Nodup holds; i.e., Icc has no duplicates.

Русский

У множества Icc a b отсутствуют дубликаты (nodup).

LaTeX

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

Lean4

theorem nodup_Icc : (Icc a b).Nodup :=
  Finset.nodup _

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

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

Разделы

Аффилиация

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