finite_iUnion_of_subsingleton — Mathlib

English

For a Subsingleton index type, the union ⋃ i s i is finite iff every s i is finite.

Русский

Для индексационного типа Subsingleton объединение ⋃ i s i конечно тогда и только тогда, когда каждый s i конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcup_i s_i\\right) \\;\\iff\\; \\forall i, \\operatorname{Finite}(s_i)$$$

Lean4

@[simp]
theorem finite_iUnion_of_subsingleton {ι : Sort*} [Subsingleton ι] {s : ι → Set α} :
    (⋃ i, s i).Finite ↔ ∀ i, (s i).Finite :=
  by
  rw [← iUnion_plift_down, finite_iUnion_iff _root_.Subsingleton.pairwise]
  simp [PLift.forall, Finite.of_subsingleton]

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