nodup_Ioc

Mathlib.Order.Interval.Multiset

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

English

(Ioc a b).Nodup.

Русский

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

LaTeX

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

Lean4

theorem nodup_Ioc : (Ioc a b).Nodup :=
  Finset.nodup _

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

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

Разделы

Аффилиация

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