accumulate_subset_accumulate

Mathlib.Data.Set.Accumulate

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

English

If x ≤ y, then Accumulate s x ⊆ Accumulate s y.

Русский

Если x ≤ y, то Accumulate s x ⊆ Accumulate s y.

LaTeX

$$$\\mathrm{Accumulate}(s,x) \\subseteq \\mathrm{Accumulate}(s,y) \\text{ whenever } x \\le y$$$

Lean4

@[gcongr]
theorem accumulate_subset_accumulate [Preorder α] {x y} (h : x ≤ y) : Accumulate s x ⊆ Accumulate s y :=
  monotone_accumulate h

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

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

Разделы

Аффилиация

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