leOnePart_eq_inv_inf_one

Mathlib.Algebra.Order.Group.PosPart

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

← MathLib Explorer

English

For any a, a⁻ᵐ equals the inverse of the minimum of a and 1: a⁻ᵐ = (min(a,1))⁻¹.

Русский

Для любого a: a⁻ᵐ = (min(a,1))⁻¹.

LaTeX

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

Lean4

@[to_additive]
theorem leOnePart_eq_inv_inf_one (a : α) : a⁻ᵐ = (a ⊓ 1)⁻¹ := by
  rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
    -- Bourbaki A.VI.12 Prop 9 d)

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

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

Разделы

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

Аффилиация

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