iUnion_accumulate — Mathlib

English

The union over all x of Accumulate s x equals the union over all x of s x.

Русский

Объединение по всех x Accumulate s x равно объединению по всех x s x.

LaTeX

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

Lean4

theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x :=
  by
  apply Subset.antisymm
  · simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
    intro z x x' ⟨_, hz⟩
    exact ⟨x', hz⟩
  · exact iUnion_mono fun i => subset_accumulate

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