eq_one_or_one_lt

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

For any a, either a = 1 or 1 < a.

Русский

Любое a либо равно 1, либо больше чем 1.

LaTeX

$$$ a = 1 \\lor 1 < a $$$

Lean4

@[to_additive]
theorem eq_one_or_one_lt (a : α) : a = 1 ∨ 1 < a :=
  (one_le a).eq_or_lt.imp_left Eq.symm

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

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

Разделы

Аффилиация

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