Iio

Mathlib.Order.Interval.Multiset

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

English

Iio(b) is the multiset of all x with x < b.

Русский

Iio(b) — мультимножество всех x, удовлетворяющих x < b.

LaTeX

$$$\mathrm{Iio}(b) = (\mathrm{Finset.Iio}(b)).\mathrm{val}$$$

Lean4

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

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

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

Разделы

Аффилиация

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