inv_Ioi₀

Mathlib.Algebra.Order.Group.Pointwise.Interval

URI: https://scilib.ai/kg/mathlib#Set.inv_Ioi₀

English

For a > 0, the inverse of Ioi(a) is Ioo(0, a^{-1}).

Русский

Для a > 0 обратное множества Ioi(a) равно Ioo(0, a^{-1}).

LaTeX

$$$ (Ioi(a))^{-1} = Ioo(0, a^{-1}) $$$

Lean4

theorem inv_Ioi₀ (ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹ := by
  rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]

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

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

Разделы

Аффилиация

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