toWeakSpaceCLM_eq_toWeakSpace — Mathlib

English

The underlying function of the canonical continuous linear map to WeakSpace agrees with the canonical weak-space embedding.

Русский

Функционал канонического непрерывного линейного отображения в WeakSpace совпадает с каноничным вложением слабого пространства.

LaTeX

$$$toWeakSpaceCLM\\ 𝕜\\ E\\ x = toWeakSpace\\ 𝕜\\ E\\ x$$$

Lean4

@[simp]
theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) : toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl

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