Set.monotone_accumulate

theorem Set.monotone_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α], Monotone (Set.Accumulate s)

The theorem `Set.monotone_accumulate` states that for any type `α` with a preorder structure and any function `s` from `α` to sets of type `β`, the operation `Set.Accumulate s` is monotone. In other words, if `x ≤ y` for two elements `x`, `y` of type `α`, then `Set.Accumulate s x` is a subset of `Set.Accumulate s y`. Here, `Set.Accumulate s x` is defined to be the union of `s z` for all `z` in `α` such that `z ≤ x`.

More concisely: For any preorder (α, ≤) and function s : α → Sets (β), the operation Set.Accumulate s is monotone, that is, Set.Accumulate s x ⊆ Set.Accumulate s y for all x ≤ y in α.