IsSemilinearSet — Mathlib

English

A set is semilinear if it is a finite union of linear sets.

Русский

Множество семилинейно, если оно является конечным объединением линейных множеств.

LaTeX

$$$IsSemilinearSet(s) \iff \exists S : Set(Set M), S.Finite \land (\forall t \in S, IsLinearSet t) \land s = ⋃₀ S.$$$

Lean4

/-- A set is semilinear if it is a finite union of linear sets. -/
def IsSemilinearSet (s : Set M) : Prop :=
  ∃ (S : Set (Set M)), S.Finite ∧ (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ S

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