lt_of_mul_lt_mul_of_le₀ — Mathlib

English

If a b < c d with c > 0 and c ≤ a, then b < d.

Русский

Если a b < c d и c > 0, и c ≤ a, тогда b < d.

LaTeX

$$$\\\\forall a,b,c,d \\\\in \\\\alpha, \\\\ a b < c d \\\\land 0 < c \\\\land c \\\\le a \\\\Rightarrow b < d$$$

Lean4

theorem lt_of_mul_lt_mul_of_le₀ (h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d :=
  by
  have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
  rw [← inv_le_inv₀ (zero_lt_iff.2 ha) hc] at hh
  simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne'] using
    mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le' (inv_pos.2 hc)

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