finite_biUnion' — Mathlib

English

Dependent finite biUnion over a finite index: the union ⋃ x ∈ s, t x is finite given all fibres finite.

Русский

Зависимое конечное биобъединение: объединение ⋃ x ∈ s, t x конечно при условии, что каждое множество-фибер конечное.

LaTeX

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

Lean4

instance finite_biUnion' {ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α) [∀ i, Finite (t i)] :
    Finite (⋃ x ∈ s, t x) :=
  finite_biUnion s t fun _ _ => inferInstance

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