English
Let E be a normed inner product space over 𝕜 with a Loewner order defined on operators. For f,g ∈ End(E) that are continuous linear maps, the natural order on endomorphisms induced by the underlying linear maps agrees with the Loewner order on continuous linear maps; i.e., (f viewed as a linear map) ≤ g if and only if f ≤ g in the continuous-linear-map order.
Русский
Пусть E — нормированное иннерположение над полем 𝕜, на отображениях введён порядок Лоуэнера. Для f,g ∈ End(E) нормированные линейные отображения удовлетворяют: (f как линейное отображение) ≤ g тогда и только тогда, когда f ≤ g в порядке непрерывно линейных отображений.
LaTeX
$$$(f : E \to_\mathbb{K} E) \le g \;\Longleftrightarrow\; f \le g$$$
Lean4
theorem coe_le_coe_iff (f g : E →L[𝕜] E) : (f : E →ₗ[𝕜] E) ≤ g ↔ f ≤ g :=
isPositive_toLinearMap_iff (g - f)
