English
If s is a finite set of indices and t: ι → Set α, with each t i finite for i ∈ s, then the biUnion ⋃_{i ∈ s} t i is finite.
Русский
Если s — конечное множество индексов и t : ι → Set α, при этом для каждого i ∈ s множество t i конечно, то объединение ⋃_{i ∈ s} t i конечно.
LaTeX
$$$\\operatorname{Finite}\\left(\\bigcup_{i \\in s} t(i)\\right)$$$
Lean4
/-- A union of sets with `Fintype` structure over a set with `Fintype` structure has a `Fintype`
structure. -/
def fintypeBiUnion [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s] (t : ι → Set α) (H : ∀ i ∈ s, Fintype (t i)) :
Fintype (⋃ x ∈ s, t x) :=
haveI : ∀ i : toFinset s, Fintype (t i) := fun i => H i (mem_toFinset.1 i.2)
Fintype.ofFinset (s.toFinset.attach.biUnion fun x => (t x).toFinset) fun x => by simp
