inducedMap_nonneg — Mathlib

English

Let a be nonnegative in the ordered field α. Then the induced map to β sends a to a nonnegative element: 0 ≤ inducedMap α β a.

Русский

Пусть a неотрицательно в упорядоченном поле α. Тогда индуцированное отображение отправляет a в неотрицательное в β: 0 ≤ inducedMap α β a.

LaTeX

$$$0 \\le \\operatorname{inducedMap}_{\\alpha,\\beta}(a)$$$

Lean4

theorem inducedMap_nonneg (ha : 0 ≤ a) : 0 ≤ inducedMap α β a :=
  (inducedMap_zero α _).ge.trans <| inducedMap_mono _ _ ha

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