rank_span_set — Mathlib

English

For a linearly independent set indexed by v with a subset s, the toENat of the rank of span of v''s image equals the encard of s.

Русский

Для линейно независимого множества, индексированного v, и подмножества s, toENat ранга порождаемого span(v''s) равен encard(s).

LaTeX

$$\n(\\operatorname{rank}_R(\\operatorname{span}_R( (v'' )s )).toENat = s.encard\n$$

Lean4

theorem rank_span_set {s : Set M} (hs : LinearIndepOn R id s) : Module.rank R ↑(span R s) = #s :=
  by
  rw [← @setOf_mem_eq _ s, ← Subtype.range_coe_subtype]
  exact rank_span hs

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