Ioi

Mathlib.Order.Interval.Multiset

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

English

Ioi(a) is the multiset of all elements x with a < x.

Русский

Ioi(a) — мультимножество всех элементов x с условием a < x.

LaTeX

$$$\mathrm{Ioi}(a) = (\mathrm{Finset.Ioi}(a)).\mathrm{val}$$$

Lean4

/-- The multiset of elements `x` such that `a < x`. Basically `Set.Ioi a` as a multiset. -/
def Ioi (a : α) : Multiset α :=
  (Finset.Ioi a).val

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

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

Разделы

Аффилиация

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