mk_le_mk

Mathlib.GroupTheory.MonoidLocalization.Order

URI: https://scilib.ai/kg/mathlib#Localization.mk_le_mk

English

The inequality mk a1 a2 ≤ mk b1 b2 is equivalent to the cross-product inequality ↑b2 · a1 ≤ a2 · b1.

Русский

Неравенство mk a1 a2 ≤ mk b1 b2 эквивалентно произведению: ↑b2 · a1 ≤ a2 · b1.

LaTeX

$$$mk\\ a_1 a_2 \\le mk\\ b_1 b_2 \\iff \\uparrow b_2 \\cdot a_1 \\le a_2 \\cdot b_1$$$

Lean4

@[to_additive]
theorem mk_le_mk : mk a₁ a₂ ≤ mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ a₂ * b₁ :=
  Iff.rfl

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

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

Разделы

Аффилиация

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