Iic

Mathlib.Order.Interval.Multiset

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

English

Iic(b) is the multiset of all x with x ≤ b.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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