isNonneg_def — Mathlib

English

A sesquilinear map is nonnegative if and only if it evaluates to a nonnegative scalar on every vector.

Русский

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

LaTeX

$$$\\mathrm{IsNonneg}(B) \\iff \\forall x, 0 \\le B(x,x)$$$

Lean4

theorem isNonneg_def [LE R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R} : B.IsNonneg ↔ ∀ x, 0 ≤ B x x :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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