extendLe_apply_self — Mathlib

English

If hs is a linear independence condition on s, then for any subset relation hst, ht, and any x in hs.extend hst, the coordinate under the extended basis equals x itself when viewed in the ambient space.

Русский

Если hs задаёт независимость на s, и есть включение hst и ht, то каждый элемент x из hs.extend hst имеет тот же координат под базисом, что и x в исходном пространстве.

LaTeX

$$$\\text{Basis.extendLe hs hst ht}\\; x = x$$$

Lean4

theorem extendLe_apply_self (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) (x : hs.extend hst) :
    Basis.extendLe hs hst ht x = x :=
  Basis.mk_apply _ _ _

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