map_nonneg — Mathlib

English

A positive linear map sends nonnegative elements to nonnegative elements.

Русский

Положительное линейное отображение отправляет неотрицательные элементы в неотрицательные.

LaTeX

$$$x \\ge 0 \\Rightarrow f(x) \\ge 0$$$

Lean4

@[aesop safe apply (rule_sets := [CStarAlgebra])]
protected theorem map_nonneg (f : E₁ →ₚ[R] E₂) {x : E₁} (hx : 0 ≤ x) : 0 ≤ f x :=
  _root_.map_nonneg f hx

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