instCountableSubtypeMemSubmoduleSpanRange

English

If R is countable and we have a countable index set, then the span of a countable family is countable.

Русский

Если R счётно, и индексный набор счётный, то линейная оболочка счётной семьи векторoв является счётной.

LaTeX

$$$\\operatorname{Countable} \\big(\\operatorname{Submodule}.span_R(\\operatorname{Set.range} v)\\big)$$$

Lean4

/-- If `R` is countable, then any `R`-submodule spanned by a countable family of vectors is
countable. -/
instance {ι : Type*} [Countable R] [Countable ι] (v : ι → M) : Countable (Submodule.span R (Set.range v)) :=
  by
  refine
    Set.countable_coe_iff.mpr
      (Set.Countable.mono ?_ (Set.countable_range (fun c : (ι →₀ R) => c.sum fun i _ => (c i) • v i)))
  exact fun _ h => Finsupp.mem_span_range_iff_exists_finsupp.mp (SetLike.mem_coe.mp h)

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