biUnion_finset — Mathlib

English

For any finite Finset of indices, the union of sets t(i) is proper semilinear if each t(i) is.

Русский

Для любого конечного множества индексов Finset объединение множеств t(i) является правильным семилинейным, если для каждого i t(i) — правильное семилинейное.

LaTeX

$$$\forall s : Finset \iota, \forall t : \iota \rightarrow Set M, (\forall i \in s, IsProperSemilinearSet(t(i))) \Rightarrow IsProperSemilinearSet(\bigcup_{i \in s} t(i))$$$

Lean4

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

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