biUnion — Mathlib

English

A finite union of sets, each proper semilinear, is proper semilinear.

Русский

Конечное объединение множеств, каждое из которых является правильным семилинейным, также является правильным семилинейным.

LaTeX

$$$S\text{ finite} \Rightarrow (\forall s \in S, IsProperSemilinearSet(s)) \Rightarrow IsProperSemilinearSet(\bigcup S)$$$

Lean4

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

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