union — Mathlib

English

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

Русский

Если s1 и s2 семилинейны, то их объединение s1 ∪ s2 семилинейно.

LaTeX

$$$IsSemilinearSet(s_1) \rightarrow IsSemilinearSet(s_2) \rightarrow IsSemilinearSet(s_1 \cup s_2).$$$

Lean4

/-- Semilinear sets are closed under union. -/
theorem union (hs₁ : IsSemilinearSet s₁) (hs₂ : IsSemilinearSet s₂) : IsSemilinearSet (s₁ ∪ s₂) :=
  by
  rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩
  rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩
  rw [← sUnion_union]
  refine ⟨S₁ ∪ S₂, hS₁.union hS₂, fun s hs => ?_, rfl⟩
  rw [mem_union] at hs
  exact hs.elim (hS₁' s) (hS₂' s)

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