English
A linearly independent family is maximal when no strictly larger linearly independent family exists; equivalently, extending the index set while preserving independence cannot enlarge the span.
Русский
Линейно независимое семейство называется максимальным, если не существует строго большего линейно независимого семейства; эквивалентно тому, что расширение множества координат сохраняющей независимость не расширяет порождающее пространство.
LaTeX
$$Maximal(v) := ∀ (s : Set M) (_i' : LinearIndependent R ((↑) : s → M)) (_h : range v ≤ s), range v = s$$
Lean4
/-- A linearly independent family is maximal if there is no strictly larger linearly independent family.
-/
@[nolint unusedArguments]
def Maximal {ι : Type w} {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M}
(_i : LinearIndependent R v) : Prop :=
∀ (s : Set M) (_i' : LinearIndependent R ((↑) : s → M)) (_h : range v ≤ s), range v = s
