add — Mathlib

English

If s1 and s2 are semilinear, then s1 + s2 is semilinear.

Русский

Если s1 и s2 семилинейны, то s1 + s2 семилинейно.

LaTeX

$$$IsSemilinearSet(s_1) \land IsSemilinearSet(s_2) \Rightarrow IsSemilinearSet(s_1 + s_2).$$$

Lean4

/-- Semilinear sets are closed under set addition. -/
theorem add (hs₁ : IsSemilinearSet s₁) (hs₂ : IsSemilinearSet s₂) : IsSemilinearSet (s₁ + s₂) :=
  by
  rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩
  rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩
  simp_rw [sUnion_add, add_sUnion]
  exact biUnion hS₁ fun s₁ hs₁ => biUnion hS₂ fun s₂ hs₂ => ((hS₁' s₁ hs₁).add (hS₂' s₂ hs₂)).isSemilinearSet

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