isPositive_ofNat

Mathlib.Analysis.InnerProductSpace.Positive

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

English

For any natural n with at least two, the operator ofNat(n) acts positively.

Русский

Для любого n ≥ 2 оператор ofNat(n) действует положительно.

LaTeX

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

Lean4

@[simp]
theorem isPositive_ofNat {n : ℕ} [n.AtLeastTwo] : IsPositive (ofNat(n) : E →L[𝕜] E) :=
  isPositive_natCast

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

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

Разделы

Аффилиация

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