inv_Iio₀

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

If a < 0, then (Iio a)⁻¹ = Ioo a⁻¹ 0.

Русский

Если a < 0, то (Iio a)⁻¹ = Ioo a⁻¹ 0.

LaTeX

$$$(\mathrm{Iio}(a))^{-1} = \mathrm{Ioo}(a^{-1}, 0)$$$

Lean4

theorem inv_Iio₀ {a : α} (ha : a < 0) : (Iio a)⁻¹ = Ioo a⁻¹ 0 := by
  rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]

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

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

Разделы

Аффилиация

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