min_inv_inv'

Mathlib.Algebra.Order.Group.MinMax

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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