ofSpan_apply_self — Mathlib

English

If x is taken from the index set used to build Basis.ofSpan, then Basis.ofSpan hs x equals x.

Русский

Если x принадлежит индексу, используемому в Basis.ofSpan, то Basis.ofSpan hs x равно x.

LaTeX

$$$x \\in (\\text{linearIndepOn\_empty } K\\ id)\\.extend(\\emptysubset s) \\Rightarrow \\mathrm{Basis.ofSpan}(hs)\\,x = x$$$

Lean4

theorem ofSpan_apply_self (hs : ⊤ ≤ span K s) (x : (linearIndepOn_empty K id).extend (empty_subset s)) :
    Basis.ofSpan hs x = x :=
  extendLe_apply_self (linearIndependent_empty K V) (empty_subset s) hs x

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