eq_one_of_one_le_mul_left

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#eq_one_of_one_le_mul_left

← MathLib Explorer

English

If a ≤ 1 and b ≤ 1 and 1 ≤ a·b, then a = 1.

Русский

Если a ≤ 1 и b ≤ 1 и 1 ≤ a·b, то a = 1.

LaTeX

$$$(a \\le 1) \\\\land (b \\le 1) \\\\land (1 \\le a \\\\cdot b) \\\\Rightarrow a = 1$$$

Lean4

@[to_additive eq_zero_of_add_nonneg_left]
theorem eq_one_of_one_le_mul_left (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : a = 1 :=
  ha.eq_of_not_lt fun h => hab.not_gt <| mul_lt_one_of_lt_of_le h hb

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

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

Разделы

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

Аффилиация

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