continuous_coe_repr — Mathlib

English

Let B be a finite basis of a normed space M over a nontrivial normed field R. Then the map that assigns to each vector its coordinate vector in B is continuous.

Русский

Пусть B — конечная база нормированного пространства M над ненулевым нормованным полем R. Тогда отображение, отправляющее вектор на его координаты в базе B, непрерывно.

LaTeX

$$$\\text{Continuous}\\big(m \\mapsto B.\\operatorname{repr}(m)\\big)$$$

Lean4

theorem continuous_coe_repr : Continuous (fun m : M => ⇑(B.repr m)) :=
  have := Finite.of_basis B
  LinearMap.continuous_of_finiteDimensional B.equivFun.toLinearMap

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