nodup_Ioo

Mathlib.Order.Interval.Multiset

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

English

(Ioo a b).Nodup.

Русский

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

LaTeX

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

Lean4

theorem nodup_Ioo : (Ioo a b).Nodup :=
  Finset.nodup _

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

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

Разделы

Аффилиация

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