biUnion_mem — Mathlib

English

An algebra is closed under finite unions.

Русский

Алгебра замкнута относительно конечных объединений.

LaTeX

$$$\\forall S : Finset, (\\forall i \\in S, s_i \\in 𝒜) \\Rightarrow \\bigcup_{i \\in S} s_i \\in 𝒜$$$

Lean4

/-- An algebra of sets is closed by finite unions. -/
theorem biUnion_mem {ι : Type*} (h𝒜 : IsSetAlgebra 𝒜) {s : ι → Set α} (S : Finset ι) (hs : ∀ i ∈ S, s i ∈ 𝒜) :
    ⋃ i ∈ S, s i ∈ 𝒜 :=
  h𝒜.isSetRing.biUnion_mem S hs

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