sqLe_add_mixed — Mathlib

English

If SqLe x c y d and SqLe z c w d, then c (x z) ≤ d (y w).

Русский

Если SqLe x c y d и SqLe z c w d, тогда c (x z) ≤ d (y w).

LaTeX

$$$\mathrm{SqLe} x c y d \land \mathrm{SqLe} z c w d \Rightarrow c \cdot (x \cdot z) \le d \cdot (y \cdot w)$$$

Lean4

theorem sqLe_add_mixed {c d x y z w : ℕ} (xy : SqLe x c y d) (zw : SqLe z c w d) : c * (x * z) ≤ d * (y * w) :=
  Nat.mul_self_le_mul_self_iff.1 <| by simpa [mul_comm, mul_left_comm] using Nat.mul_le_mul xy zw

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