accumulate_mem — Mathlib

English

For a sequence of sets s(n) ∈ C, the accumulated set Accumulate s n lies in C for every n.

Русский

Для последовательности множеств s(n) ∈ C, Accumulate s n ∈ C для каждого n.

LaTeX

$$$\forall n,\ Accumulate\, s\, n \in C.$$$

Lean4

theorem accumulate_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ i, s i ∈ C) (n : ℕ) : Accumulate s n ∈ C := by
  induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)

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