isPosSemidef_def — Mathlib

English

A sesquilinear form B is positive semidefinite if and only if B is symmetric and nonnegative.

Русский

Сесквилинейная форма B положительно полусобственна тогда, когда она симметрична и неотрицательна.

LaTeX

$$$\text{IsPosSemidef}(B) \iff (\text{IsSymm}(B) \land \text{IsNonneg}(B))$$$

Lean4

theorem isPosSemidef_def [LE R] {B : M →ₛₗ[I₁] M →ₗ[R] R} : B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg :=
  ⟨fun h ↦ ⟨h.isSymm, h.isNonneg⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

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