English
Let R satisfy the strong rank condition. If v is a linearly independent family v: ι → M and w is a spanning subset of M (span_R w = ⊤), then the indexing cardinality does not exceed the spanning cardinality: |ι| ≤ |w|.
Русский
Пусть R удовлетворяет условию сильной ранговости. Если v: ι → M линейно независимо и w порождает полумодуль M (span_R w = ⊤), то кардинал множества индексов не больше кардинала множества w: |\iota| ≤ |w|.
LaTeX
$$$|\\iota| \\le |w|$$$
Lean4
/-- If `R` satisfies the strong rank condition, then for any linearly independent family `v : ι → M`
and spanning set `w : Set M`, the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem linearIndependent_le_span'' {ι : Type v} {v : ι → M} (i : LinearIndependent R v) (w : Set M)
(s : span R w = ⊤) : #ι ≤ #w := by
fapply card_le_of_injective'' (R := R)
· apply Finsupp.linearCombination
exact fun i ↦ Span.repr R w ⟨v i, s ▸ trivial⟩
· intro f g h
apply_fun linearCombination R ((↑) : w → M) at h
simp only [linearCombination_linearCombination, Span.finsupp_linearCombination_repr] at h
exact i h
