continuous_toMatrix — Mathlib

English

For a finite basis B of a normed space M over R, the map sending a family v: ι → M to the matrix B.toMatrix v is continuous.

Русский

Для базы B конечного размера нормированного пространства M над R отображение, отправляющее семейство векторов v: ι → M в матрицу B.toMatrix v, непрерывно.

LaTeX

$$$\\text{Continuous}\\big(v \\mapsto B.toMatrix(v)\\big)$$$

Lean4

theorem continuous_toMatrix : Continuous fun (v : ι → M) => B.toMatrix v :=
  let _ := Fintype.ofFinite ι
  have := Finite.of_basis B
  LinearMap.continuous_of_finiteDimensional B.toMatrixEquiv.toLinearMap

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