biUnion_accumulate — Mathlib

English

For any x, the union over y ≤ x of Accumulate s y equals the union over y ≤ x of s y.

Русский

Для любого x выполняется: ⋃_{y ≤ x} Accumulate(s, y) = ⋃_{y ≤ x} s(y).

LaTeX

$$$\\bigcup_{y \\le x} \\mathrm{Accumulate}(s,y) = \\bigcup_{y \\le x} s(y)$$$

Lean4

theorem biUnion_accumulate [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y :=
  by
  apply Subset.antisymm
  · exact iUnion₂_subset fun y hy => monotone_accumulate hy
  · exact iUnion₂_mono fun y _ => subset_accumulate

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