English
Let M be an additive commutative monoid. A subset s ⊆ M is called a proper linear set if there exist an element a ∈ M and a finite subset t ⊆ M such that s is the translate by a of the submonoid generated by t, i.e. s = a + closure(t), where t is linearly independent over the natural numbers.
Русский
Пусть M — коммутативный аддитивный моноид. Подмножество s ⊆ M называют правильным линейным множеством, если существует элемент a ∈ M и конечное подмножество t ⊆ M такое, что s является переносом a на подсм monoid, порожденный t, то есть s = a + closure(t), причём t линейно независимо над натуральными числами.
LaTeX
$$$IsProperLinearSet(s) \iff \exists a \in M, \exists t \subseteq M, Finite(t) \land LinearIndepOn(\mathbb{N}, \mathrm{id}, t) \land s = a +^\vee (\overline{t})$$$
Lean4
/-- A linear set is proper if its submonoid generators (periods) are linearly independent. -/
def IsProperLinearSet (s : Set M) : Prop :=
∃ (a : M) (t : Set M), t.Finite ∧ LinearIndepOn ℕ id t ∧ s = a +ᵥ (closure t : Set M)
