snd_inv — Mathlib

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

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