sUnion — Mathlib

English

If s is a finite set of sets and every member t ∈ s is finite, then the sUnion of s is finite.

Русский

Если s — конечное множество множеств и каждое t ∈ s конечно, то sUnion s конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcup_{t \\in s} t\\right)$$$

Lean4

theorem sUnion {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, Set.Finite t) : (⋃₀ s).Finite := by
  simpa only [sUnion_eq_biUnion] using hs.biUnion H

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