English
Let s be a nonempty interval in a commutative group α with a partial order and an ordered monoid structure. Then the right endpoint of the inverse interval s^{-1} equals the inverse of the left endpoint of s, i.e. snd(s^{-1}) = (fst(s))^{-1}.
Русский
Пусть s — непустой интервал в группе α с частичным порядком и упорядоченным моноидом. Тогда правая граница обратного интервала s^{-1} равна обратному левой границе s, т.е. snd(s^{-1}) = (fst(s))^{-1}.
LaTeX
$$$ \operatorname{snd}(s^{-1}) = (\operatorname{fst}(s))^{-1} $$$
Lean4
@[to_additive (attr := simp)]
theorem snd_inv : s⁻¹.snd = s.fst⁻¹ :=
rfl