oneLePart_lt

Mathlib.Algebra.Order.Group.PosPart

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

English

The relation a⁺ᵐ < b is equivalent to a < b and 1 < b.

Русский

Отношение a⁺ᵐ < b эквивалентно a < b и 1 < b.

LaTeX

$$a^{+m} < b \iff a < b ∧ 1 < b$$

Lean4

@[to_additive (attr := simp)]
theorem oneLePart_lt : a⁺ᵐ < b ↔ a < b ∧ 1 < b :=
  sup_lt_iff

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

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

Разделы

Аффилиация

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