inv_Ioo

Mathlib.Algebra.Order.Group.Pointwise.Interval

URI: https://scilib.ai/kg/mathlib#Set.inv_Ioo

English

Inverting an open interval (Ioo a b) yields (Ioo b^{-1} a^{-1}).

Русский

Обратное изображение открытого интервала (Ioo a b) равно Ioo b^{-1} a^{-1}.

LaTeX

$$$$(Ioo\\ a\\ b)^{-1} = Ioo\\ b^{-1}\\ a^{-1}$$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_Ioo (a b : α) : (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹ := by simp [← Ioi_inter_Iio, inter_comm]

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

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

Разделы

Аффилиация

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