preimage_add_const_Ioi

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

The inverse of Ioo(a,b) is Ioo(b^{-1}, a^{-1}).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_add_const_Ioi : (fun x => x + a) ⁻¹' Ioi b = Ioi (b - a) :=
  ext fun _x => sub_lt_iff_lt_add.symm

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

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

Разделы

Аффилиация

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