basis — Mathlib

English

The function h.basis, when coerced to a function, equals the original index map e; i.e., ⇑h.basis = e.

Русский

Преобразование h.basis в функцию даёт исходное отображение e; то есть ⇑h.basis = e.

LaTeX

$$$ \\text{coe}_\\text{basis} : (h.basis) = e $$$

Lean4

/-- `(h : DualBases e ε).basis` shows the family of vectors `e` forms a basis. -/
@[simps repr_apply, simps -isSimp repr_symm_apply]
def basis : Basis ι R M :=
  Basis.ofRepr
    { toFun := coeffs h
      invFun := lc e
      left_inv := lc_coeffs h
      right_inv := coeffs_lc h
      map_add' := fun v w => by
        ext i
        exact (ε i).map_add v w
      map_smul' := fun c v => by
        ext i
        exact (ε i).map_smul c v }

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