toWeakSpaceCLM_bijective — Mathlib

English

The canonical weak-space continuous linear map is bijective, hence an isomorphism.

Русский

Каноническое непрерывное линейное отображение слабого пространства является биективным, следовательно изоморфизм.

LaTeX

$$$toWeakSpaceCLM\\ 𝕜\\ E\\ \\text{ is bijective}$$$

Lean4

theorem toWeakSpaceCLM_bijective : Function.Bijective (toWeakSpaceCLM 𝕜 E) :=
  (toWeakSpace 𝕜 E).bijective

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