biUnion' — Mathlib

English

Dependent version of Finite.biUnion: if s is finite and t : ∀ i ∈ s, Set α is such that each t i hi is finite, then ⋃ i ∈ s, t i hi is finite.

Русский

Зависимое обобщение Finite.biUnion: если s конечен и t i hi конечны для каждого i ∈ s, то ⋃ i ∈ s, t i hi конечен.

LaTeX

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

Lean4

/-- Dependent version of `Finite.biUnion`. -/
theorem biUnion' {ι} {s : Set ι} (hs : s.Finite) {t : ∀ i ∈ s, Set α} (ht : ∀ i (hi : i ∈ s), (t i hi).Finite) :
    (⋃ i ∈ s, t i ‹_›).Finite := by
  have := hs.to_subtype
  rw [biUnion_eq_iUnion]
  apply finite_iUnion fun i : s => ht i.1 i.2

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