toNonnegHomClass — Mathlib

English

A map f is monotone iff it sends nonnegative elements to nonnegative elements.

Русский

Любое отображение f монотонно тогда и только тогда, когда оно неотрицательное на неотрицательных аргументах.

LaTeX

$$$\text{Monotone}(f) \iff \forall a \ge 0, f(a) \ge 0$$$

Lean4

instance (priority := 100) toNonnegHomClass [NonUnitalNonAssocRing α] [Semiring β] [LinearOrder β]
    [IsOrderedAddMonoid β] [RingSeminormClass F α β] : NonnegHomClass F α β :=
  AddGroupSeminormClass.toNonnegHomClass

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