isPosSemidef_def — Mathlib

English

A bilinear form is positive semidefinite if and only if it is symmetric and nonnegative.

Русский

Билинейная форма положительно полуположна если и только если она симметрична и неотрицательна.

LaTeX

$$B.IsPosSemidef \iff (B.IsSymm ∧ B.IsNonneg)$$

Lean4

theorem isPosSemidef_def [LE R] : B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg :=
  ⟨fun h ↦ ⟨h.isSymm, h.isNonneg⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

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