oneLePart_of_one_lt_oneLePart

Mathlib.Algebra.Order.Group.PosPart

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

← MathLib Explorer

English

If 1 < a⁺ᵐ, then a⁺ᵐ = a.

Русский

Если 1 < a⁺ᵐ, то a⁺ᵐ = a.

LaTeX

$$1 < a^{+m} \Rightarrow a^{+m} = a$$

Lean4

@[to_additive posPart_eq_of_posPart_pos]
theorem oneLePart_of_one_lt_oneLePart (ha : 1 < a⁺ᵐ) : a⁺ᵐ = a := by rw [oneLePart_def, right_lt_sup, not_le] at ha;
  exact oneLePart_eq_self.2 ha.le

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

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

Разделы

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

Аффилиация

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