fintypeBiUnion' — Mathlib

English

A dependent version of finite union: if s is finite and for every i ∈ s the set t i hi is finite, then the union ⋃_{i ∈ s} t i hi is finite.

Русский

Зависимая версия конечного объединения: если s конечен и для каждого i ∈ s множество t(i, hi) конечно, то объединение ⋃_{i ∈ s} t(i, hi) конечно.

LaTeX

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

Lean4

instance fintypeBiUnion' [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s] (t : ι → Set α) [∀ i, Fintype (t i)] :
    Fintype (⋃ x ∈ s, t x) :=
  Fintype.ofFinset (s.toFinset.biUnion fun x => (t x).toFinset) <| by simp

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