isPositive_natCast

Mathlib.Analysis.InnerProductSpace.Positive

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.isPositive_natCast

English

For every natural number n, the operator n acting as scalar multiplication is positive.

Русский

Для каждого натурального числа n оператор умножения на n положителен.

LaTeX

$$$\text{IsPositive} (n: E \to_L[\mathbb{K}] E)$$$

Lean4

@[simp]
theorem isPositive_natCast {n : ℕ} : IsPositive (n : E →L[𝕜] E) :=
  (isPositive_toLinearMap_iff _).mp LinearMap.isPositive_natCast

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru