mk₀ — Mathlib

English

From a linear map with a nonnegativity-preserving predicate hf, one obtains a PositiveLinearMap.

Русский

Из линейного отображения с условием сохранения неотрицательности hfConstructed получается положительное линейное отображение.

LaTeX

$$$\\mathrm{mk}_0(f,hf) : E_1 \\to_{R}^{+} E_2$$$

Lean4

/-- Define a positive map from a linear map that maps nonnegative elements to nonnegative
elements -/
def mk₀ (f : E₁ →ₗ[R] E₂) (hf : ∀ x, 0 ≤ x → 0 ≤ f x) : E₁ →ₚ[R] E₂ :=
  { f with
    monotone' := by
      intro a b hab
      rw [← sub_nonneg] at hab ⊢
      have : 0 ≤ f (b - a) := hf _ hab
      simpa using this }

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