biUnion_finset — Mathlib

English

A finite Finset of semilinear sets yields a semilinear union.

Русский

Конечное множество Finset линейных множеств даёт линейное объединение.

LaTeX

$$$ht : \forall i \in s, IsSemilinearSet (t i) \Rightarrow IsSemilinearSet (⋃ i ∈ s, t i).$$$

Lean4

theorem biUnion_finset {s : Finset ι} {t : ι → Set M} (ht : ∀ i ∈ s, IsSemilinearSet (t i)) :
    IsSemilinearSet (⋃ i ∈ s, t i) :=
  biUnion s.finite_toSet ht

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