isLinearSet_iff — Mathlib

English

IsLinearSet s if and only if there exists a and a finitely generated submonoid P such that s = a +ᵥ P.

Русский

IsLinearSet s эквивалентно существованию a и FG-подмножества P так, что s = a +ᵥ P.

LaTeX

$$$ IsLinearSet s \\iff \\exists a \\exists P, P.FG \\wedge s = a +ᵥ (P : Set M) $$$

Lean4

/-- An equivalent expression of `IsLinearSet` in terms of `Finset` instead of `Set.Finite`. -/
theorem isLinearSet_iff : IsLinearSet s ↔ ∃ (a : M) (t : Finset M), s = a +ᵥ (closure (t : Set M) : Set M) := by
  simp [IsLinearSet, Finset.exists]

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