map_add_right_Icc — Mathlib

English

In a commutative group with order, an element a⁻¹ lies in the closed interval [c,d] if and only if a lies in the reflected interval [d⁻¹,c⁻¹].

Русский

В группе с порядком: элемент a⁻¹ принадлежит интервалу [c,d], если и только если a принадлежит интервалу [d⁻¹,c⁻¹].

LaTeX

$$$a^{-1} \in \mathrm{Icc}(c,d) \iff a \in \mathrm{Icc}(d^{-1}, c^{-1})$$$

Lean4

theorem map_add_right_Icc (a b c : α) : ((Icc a b).map fun x => x + c) = Icc (a + c) (b + c) :=
  by
  simp_rw [add_comm _ c]
  exact map_add_left_Icc _ _ _

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