biUnion — Mathlib

English

If s is finite and each t(i) is semilinear, then the union ⋃ i∈s t(i) is semilinear.

Русский

Если s конечно, и каждый t(i) семилинейно, то ⋃ i∈s t(i) семилинейно.

LaTeX

$$$(s).Finite \rightarrow (\forall i \in s, IsSemilinearSet (t i)) \rightarrow IsSemilinearSet (⋃ i ∈ s, t i).$$$

Lean4

theorem biUnion {s : Set ι} {t : ι → Set M} (hs : s.Finite) (ht : ∀ i ∈ s, IsSemilinearSet (t i)) :
    IsSemilinearSet (⋃ i ∈ s, t i) := by
  rw [← sUnion_image]
  apply sUnion (hs.image t)
  simpa

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