biUnion — Mathlib

English

A finite union of finitely many sets over a finite index set is finite: (⋃ i ∈ s, t i).

Русский

Конечное объединение конечного числа множеств по конечному индексу конечно.

LaTeX

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

Lean4

theorem biUnion {ι} {s : Set ι} (hs : s.Finite) {t : ι → Set α} (ht : ∀ i ∈ s, (t i).Finite) : (⋃ i ∈ s, t i).Finite :=
  hs.biUnion' ht

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