subset_accumulate

Mathlib.Data.Set.Accumulate

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

English

For every x, s(x) is contained in Accumulate s x.

Русский

Для каждого x выполняется s(x) ⊆ Accumulate s x.

LaTeX

$$$s(x) \\subseteq \\mathrm{Accumulate}(s,x)$$$

Lean4

theorem subset_accumulate [Preorder α] {x : α} : s x ⊆ Accumulate s x := fun _ => mem_biUnion le_rfl

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

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

Разделы

Аффилиация

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