iUnion — Mathlib

English

If ι is finite and each s(i) is semilinear, then the indexed union ⋃ i IsSemilinearSet(s(i)) is semilinear.

Русский

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

LaTeX

$$$[Finite \ ι] \to (\forall i, IsSemilinearSet (s i)) \Rightarrow IsSemilinearSet (Set.iUnion fun i => s i).$$$

Lean4

theorem iUnion [Finite ι] {s : ι → Set M} (hs : ∀ i, IsSemilinearSet (s i)) : IsSemilinearSet (⋃ i, s i) :=
  by
  rw [← sUnion_range]
  apply sUnion (finite_range s)
  simpa

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