sUnion — Mathlib

English

If S is finite and each t(i) is a proper semilinear set, then the union over i in S of t(i) is also a proper semilinear set.

Русский

Если S конечен и каждый t(i) является правильным семилинейным множеством, то объединение по i из S множества t(i) также является правильным семилинейным множеством.

LaTeX

$$$s.Finite \land (\forall i \in s, IsProperSemilinearSet(t(i))) \Rightarrow IsProperSemilinearSet(\bigcup_{i \in s} t(i))$$$

Lean4

theorem sUnion {S : Set (Set M)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsProperSemilinearSet s) :
    IsProperSemilinearSet (⋃₀ S) := by
  induction S, hS using Finite.induction_on with
  | empty => simp
  | insert S _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa using hS'.1.union (ih hS'.2)

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