iUnion_le_mem — Mathlib

English

For a finite index set, the union up to n lies in C if each s(i) ∈ C.

Русский

Для конечного множества индексов, объединение до n лежит в C, если для каждого i ≤ n s(i) ∈ C.

LaTeX

$$$\text{If } s(n)\in C\ \forall n, \text{ then } \bigcup_{i≤n} s(i)\in C.$$$

Lean4

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

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