English
A subset s ⊆ M is a proper linear set if and only if there exists a ∈ M and a finite subset t ⊆ M such that t is linearly independent and s = a + closure(t).
Русский
Подмножество s ⊆ M является правильным линейным множеством тогда и только тогда, существует a ∈ M и конечное подмножество t ⊆ M, такое что t линейно независимо, и s = a + closure(t).
LaTeX
$$$IsProperLinearSet(s) \iff \exists a \in M, \exists t \in \mathrm{Finset}(M), LinearIndepOn(\mathbb{N}, \mathrm{id}, (t : Set M)) \land s = a +^\vee (closure (t : Set M))$$$
Lean4
theorem isProperLinearSet_iff :
IsProperLinearSet s ↔
∃ (a : M) (t : Finset M), LinearIndepOn ℕ id (t : Set M) ∧ s = a +ᵥ (closure (t : Set M) : Set M) :=
exists_congr fun a => ⟨fun ⟨t, ht, hs⟩ => ⟨ht.toFinset, by simpa⟩, fun ⟨t, hs⟩ => ⟨t, t.finite_toSet, hs⟩⟩
