finite_biUnion — Mathlib

English

A finite union of finite sets over a finite index family is finite: Finite (⋃ i ∈ s, t i).

Русский

Конечное объединение конечных множеств по конечному индексовому семейству конечно.

LaTeX

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

Lean4

theorem finite_biUnion {ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α) (H : ∀ i ∈ s, Finite (t i)) :
    Finite (⋃ x ∈ s, t x) := by
  rw [biUnion_eq_iUnion]
  haveI : ∀ i : s, Finite (t i) := fun i => H i i.property
  infer_instance

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