finite_iUnion — Mathlib

English

If ι is finite and f: ι → Set α with each f i finite, then the union ⋃ i f i is finite.

Русский

Если ι конечен и f: ι → Set α таково, что каждый f i конечен, то объединение ⋃ i f i конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcup_{i \\in ι} f(i)\\right)$$$

Lean4

instance finite_iUnion [Finite ι] (f : ι → Set α) [∀ i, Finite (f i)] : Finite (⋃ i, f i) :=
  by
  have : Fintype (PLift ι) := Fintype.ofFinite _
  have : ∀ i, Fintype (f i) := fun i => Fintype.ofFinite _
  classical apply (fintypeiUnion _).finite

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