IsProperSemilinearSet — Mathlib

English

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

Русский

Семилинейное множество является правильным, если оно является конечной объединением правильных линейных множеств.

LaTeX

$$$IsProperSemilinearSet(s) \iff \exists S \subseteq \mathcal{P}(M), S \text{ finite} \land (\forall t \in S, IsProperLinearSet(t)) \land s = \bigcup S$$$

Lean4

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

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