isProperSemilinearSet — Mathlib

English

Every semilinear set is a finite union of proper linear sets.

Русский

Каждое семилинейное множество равно конечному объединению правильных линейных множеств.

LaTeX

$$$IsSemilinearSet(s) \Rightarrow IsProperSemilinearSet(s)$$$

Lean4

/-- The **proper decomposition** of semilinear sets: every semilinear set is a finite union of
proper linear sets. -/
theorem isProperSemilinearSet [IsCancelAdd M] (hs : IsSemilinearSet s) : IsProperSemilinearSet s :=
  by
  rcases hs with ⟨S, hS, hS', rfl⟩
  simp_rw [sUnion_eq_biUnion]
  exact IsProperSemilinearSet.biUnion hS fun s hs => (hS' s hs).isProperSemilinearSet

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