inv_Icc — Mathlib

English

In a ordered group, inversion inverts closed intervals by reversing endpoints: (Icc a b)^{-1} = Icc b^{-1} a^{-1}.

Русский

В упорядоченной группе обратное отображение переворачивает концы закрытого интервала: (Icc a b)^{-1} = Icc b^{-1} a^{-1}.

LaTeX

$$$$(Icc\\ a\\ b)^{-1} = Icc\\ b^{-1}\\ a^{-1}$$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_Icc (a b : α) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹ := by simp [← Ici_inter_Iic, inter_comm]

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