finite_sUnion — Mathlib

English

If s is a finite collection of sets and each member t ∈ s is finite, then the sUnion of s is finite.

Русский

Если s — конечная коллекция множеств и каждое t ∈ s конечно, то ⋃₀ s конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcup s\\right) \\,\\text{(i.e. }\\bigcup_{t \\in s} t\\text{)}$$$

Lean4

instance finite_sUnion {s : Set (Set α)} [Finite s] [H : ∀ t : s, Finite (t : Set α)] : Finite (⋃₀ s) :=
  by
  rw [sUnion_eq_iUnion]
  exact @Finite.Set.finite_iUnion _ _ _ _ H

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