Ici

Mathlib.Order.Interval.Multiset

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

English

Ici(a) is the multiset of all elements x with a ≤ x.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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