mk_lt_mk

Mathlib.GroupTheory.MonoidLocalization.Order

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

English

The strict inequality in the localization follows the same cross-multiplication pattern as mk_le_mk.

Русский

Строгое неравенство в локализации следует той же схеме переноса произведений, как и для mk_le_mk.

LaTeX

$$$mk\\ a_1 a_2 < mk\\ b_1 b_2 \\iff ↑b_2 a_1 < a_2 b_1$$$

Lean4

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

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

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

Разделы

Аффилиация

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