nmul_le_nmul_right — Mathlib

English

If a ≤ b, then a ⨳ c ≤ b ⨳ c for any c; i.e., nmul is monotone in the left argument when right-multiplied by a fixed c treated via commutativity.

Русский

Если a ≤ b, то a ⨳ c ≤ b ⨳ c для любого c; то есть nmul монотонно по левому аргументу при фиксированном правом множителе.

LaTeX

$$$\\forall a,b,c \\in \\mathrm{Ordinal},\\ a \\le b \\rightarrow a \\nabla c \\le b \\nabla c$$$

Lean4

theorem nmul_le_nmul_right (h : a ≤ b) (c) : a ⨳ c ≤ b ⨳ c :=
  by
  rw [nmul_comm, nmul_comm b]
  exact nmul_le_nmul_left h c

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