le_of_mul_le_of_one_le — Mathlib

English

Let R be a ZeroLEOneClass with NeZero 1, MulPosStrictMono, and PosMulMono. For a,b,c ∈ R, if a c ≤ b and 0 ≤ b and 1 ≤ c, then a ≤ b.

Русский

Пусть R — ZeroLEOneClass с NeZero 1, MulPosStrictMono и PosMulMono. Пусть a,b,c ∈ R; если a c ≤ b, 0 ≤ b и 1 ≤ c, то a ≤ b.

LaTeX

$$$(h : a c \le b) \\land (hb : 0 \le b) \\land (hc : 1 \le c) \\Rightarrow a \le b$$$

Lean4

theorem le_of_mul_le_of_one_le [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [PosMulMono R] {a b c : R}
    (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) : a ≤ b :=
  le_of_mul_le_mul_right (h.trans <| le_mul_of_one_le_right hb hc) <| zero_lt_one.trans_le hc

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