Accumulate

Mathlib.Data.Set.Accumulate

URI: https://scilib.ai/kg/mathlib#Set.Accumulate

English

Accumulate s at x is the union over all y ≤ x of s(y).

Русский

Аккумулируемое множество Accumulate s x есть объединение по y ≤ x множества s(y).

LaTeX

$$$ \mathrm{Accumulate}[LE](s)(x) = \bigcup_{y \le x} s(y).$$$

Lean4

/-- `Accumulate s` is the union of `s y` for `y ≤ x`. -/
def Accumulate [LE α] (s : α → Set β) (x : α) : Set β :=
  ⋃ y ≤ x, s y

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

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

Разделы

Аффилиация

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