mul_mono

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.mul_mono

← MathLib Explorer

English

If a ≤ b and c ≤ d in Associates M, then a c ≤ b d.

Русский

Если a ≤ b и c ≤ d в Associates(M), то a c ≤ b d.

LaTeX

$$$ (a \le b) \land (c \le d) \Rightarrow (a c) \le (b d) $$$

Lean4

theorem mul_mono {a b c d : Associates M} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d :=
  let ⟨x, hx⟩ := h₁
  let ⟨y, hy⟩ := h₂
  ⟨x * y, by simp [hx, hy, mul_comm, mul_left_comm]⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru