instInvNonemptyInterval

Mathlib.Algebra.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#instInvNonemptyInterval

English

There is an inverse operation on NonemptyInterval α for a commutative group α, defined by s ↦ (snd^{-1}, fst^{-1}).

Русский

Существует обратная операция для NonemptyInterval α: s ↦ (snd^{-1}, fst^{-1}).

LaTeX

$$$s \mapsto (s.\mathrm{snd}^{-1}, s.\mathrm{fst}^{-1})$$$

Lean4

@[to_additive]
instance : Inv (NonemptyInterval α) :=
  ⟨fun s => ⟨(s.snd⁻¹, s.fst⁻¹), inv_le_inv' s.fst_le_snd⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru