range_ofSpan — Mathlib

English

The range of Basis.ofSpan hs is exactly the index set used for the basis.

Русский

Область определения Basis.ofSpan hs совпадает с используемым индексным множеством для базиса.

LaTeX

$$$\\operatorname{range}(\\mathrm{Basis.ofSpan}\\; hs) = (\\text{linearIndepOn\_empty } K\\ id).extend(\\emptysubset s)$$$

Lean4

theorem range_ofSpan (hs : ⊤ ≤ span K s) : range (ofSpan hs) = (linearIndepOn_empty K id).extend (empty_subset s) := by
  rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]

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