inv_mem_inv

Mathlib.Algebra.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.inv_mem_inv

English

If a is an element of a nonempty interval s, then a^{-1} is an element of the inverse interval s^{-1}.

Русский

Если a ∈ непустой интервал s, то a^{-1} ∈ s^{-1}.

LaTeX

$$$ a \in s \Rightarrow a^{-1} \in s^{-1} $$$

Lean4

@[to_additive]
theorem inv_mem_inv (ha : a ∈ s) : a⁻¹ ∈ s⁻¹ :=
  ⟨inv_le_inv' ha.2, inv_le_inv' ha.1⟩

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

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

Разделы

Аффилиация

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