isNonneg_def

Mathlib.LinearAlgebra.BilinearForm.Properties

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.isNonneg_def

English

The sum of two nonnegative bilinear forms is nonnegative.

Русский

Сумма двух неотрицательных билинейных форм неотрицательна.

LaTeX

$$B.IsNonneg → C.IsNonneg → (B + C).IsNonneg$$

Lean4

theorem isNonneg_def [LE R] {B : BilinForm R M} : B.IsNonneg ↔ ∀ x, 0 ≤ B x x :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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

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

Разделы

Аффилиация

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