preimage_const_add_Iic

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

The preimage of Iic b under x ↦ a + x is Iic(b − a).

Русский

Предобраз Iic под x ↦ a + x равен Iic(b − a).

LaTeX

$$$$(a + x)^{-1}(\\Iic b) = \\Iic(b - a)$$$$

Lean4

@[simp]
theorem preimage_const_add_Iic : (fun x => a + x) ⁻¹' Iic b = Iic (b - a) :=
  ext fun _x => le_sub_iff_add_le'.symm

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

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

Разделы

Аффилиация

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