coe_dualBasis — Mathlib

English

The function underlying the dualBasis satisfies the equality ⇑b.dualBasis = b.coord; the dual basis acts by the coordinate function.

Русский

Функция, лежащая в основе dualBasis, удовлетворяет равенству ⇑b.dualBasis = b.coord; дуальная база действует как координатная функция.

LaTeX

$$$ \text{coe}(b.dualBasis) = b.coord. $$$

Lean4

@[simp]
theorem coe_dualBasis : ⇑b.dualBasis = b.coord := by
  ext i x
  apply dualBasis_apply

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