max_inv_inv'

Mathlib.Algebra.Order.Group.MinMax

URI: https://scilib.ai/kg/mathlib#max_inv_inv'

← MathLib Explorer

English

In a commutative ordered group, max(a^{-1}, b^{-1}) = (min(a,b))^{-1}.

Русский

В коммутативной упорядоченной группе: max(a^{-1}, b^{-1}) = (min(a,b))^{-1}.

LaTeX

$$$ \max(a^{-1}, b^{-1}) = (\min(a,b))^{-1} $$$

Lean4

@[to_additive max_neg_neg]
theorem max_inv_inv' (a b : α) : max a⁻¹ b⁻¹ = (min a b)⁻¹ :=
  Eq.symm <| (@Monotone.map_min α αᵒᵈ _ _ Inv.inv a b) fun _ _ => inv_le_inv_iff.mpr

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

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

Разделы

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

Аффилиация

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