fintypesUnion — Mathlib

English

Let α be a type and s be a finite set of subsets of α. If every member t of s is finite, then the union of all members of s is finite.

Русский

Пусть α — множество. Пусть s — конечное множество подмножеств α. Если каждое t ∈ s конечно, то объединение ⋃_{t ∈ s} t конечно.

LaTeX

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

Lean4

instance fintypesUnion [DecidableEq α] {s : Set (Set α)} [Fintype s] [H : ∀ t : s, Fintype (t : Set α)] :
    Fintype (⋃₀ s) := by
  rw [sUnion_eq_iUnion]
  exact @Set.fintypeiUnion _ _ _ _ _ H

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