union — Mathlib

English

The union of two proper semilinear sets is again a proper semilinear set.

Русский

Объединение двух правильных семилинейных множеств снова является правильным семилинейным множеством.

LaTeX

$$$IsProperSemilinearSet(s_1) \land IsProperSemilinearSet(s_2) \Rightarrow IsProperSemilinearSet(s_1 \cup s_2)$$$

Lean4

theorem union (hs₁ : IsProperSemilinearSet s₁) (hs₂ : IsProperSemilinearSet s₂) : IsProperSemilinearSet (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)

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