injective_expMapBasis — Mathlib

English

The map expMapBasis is injective, being the composition of the injective expMap with the inverse of a basis isomorphism.

Русский

Отображение expMapBasis инъективно, так как является композицией инъективного expMap и обратного изоморфизма базиса.

LaTeX

$$$\text{Injective}(\expMapBasis : \mathbb{R}^{r} \to \mathbb{R}^{r})$$$

Lean4

theorem injective_expMapBasis : Function.Injective (expMapBasis : realSpace K → realSpace K) :=
  (injective_expMap K).comp (completeBasis K).equivFun.symm.injective

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