instPosMulMono — Mathlib

English

The multiplication by a nonnegative element is order-preserving on EReal.

Русский

Умножение на неотрицательное число сохраняет порядок на EReal.

LaTeX

$$∀ a,b,c ∈ EReal, a ≤ b ⇒ c a ≤ c b whenever c ≥ 0$$

Lean4

instance : PosMulMono EReal :=
  posMulMono_iff_covariant_pos.2 <|
    .mk <| by
      rintro ⟨x, x0⟩ a b h
      simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢
      exact
        h.imp_right <|
          Or.imp (And.imp_right <| And.imp_right (mul_le_mul_left' · _)) <|
            Or.imp_right <| And.imp_right <| And.imp_right (mul_le_mul_left' · _)

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