isNonneg_zero

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.isNonneg_zero

English

If the map is zero, then it is nonnegative.

Русский

Если карта нулевая, то она неотрицательна.

LaTeX

$$$\\mathrm{IsNonneg}(0) \\quad$ (for any domain) equals True$$

Lean4

@[simp]
theorem isNonneg_zero [Preorder R] : IsNonneg (0 : M →ₛₗ[I₁] M →ₛₗ[I₂] R) :=
  ⟨fun _ ↦ le_rfl⟩

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

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

Разделы

Аффилиация

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