inv_uIcc — Mathlib

English

In a commutative group with linear order, the inversion map sends the closed interval [[a, b]] to the closed interval [[a^{-1}, b^{-1}]].

Русский

В коммутативной группе с линейным порядком инверсия переводит закрытый интервал [[a, b]] в [[a^{-1}, b^{-1}]].

LaTeX

$$$ [[a, b]]^{-1} = [[a^{-1}, b^{-1}]] $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_uIcc (a b : α) : [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]] := by simp only [uIcc, inv_Icc, inv_sup, inv_inf]

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