one_le_mabs

Mathlib.Algebra.Order.Group.Unbundled.Abs

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

← MathLib Explorer

English

The modulus is at least one: 1 ≤ |a|_m for all a.

Русский

Для любого a верно: 1 ≤ |a|_м.

LaTeX

$$1 \le |a|_m$$

Lean4

@[to_additive (attr := simp) abs_nonneg]
theorem one_le_mabs (a : α) : 1 ≤ |a|ₘ := by
  apply pow_two_semiclosed _
  rw [mabs, pow_two, mul_sup, sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]
  apply le_sup_right

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

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

Разделы

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

Аффилиация

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