existsMulOfLe — Mathlib

English

There exists a right-multiplicative witness for inequalities: in Multiplicative α, existence of a witness c with a ≤ b · c corresponding to the additive version exists_add_of_le.

Русский

Существует доказательство по правому умножению для неравенств: в Multiplicative α существует свидетель c, такой что a ≤ b · c, соответствующее аддитивной версии exists_add_of_le.

LaTeX

$$ExistsMulOfLE (Multiplicative α)$$

Lean4

instance existsMulOfLe [Add α] [LE α] [ExistsAddOfLE α] : ExistsMulOfLE (Multiplicative α) :=
  ⟨@exists_add_of_le α _ _ _⟩

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