preimage_sub_const_Iic

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_sub_const_Iic : (fun x => x - a) ⁻¹' Iic b = Iic (b + a) := by simp [sub_eq_add_neg]

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

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

Разделы

Аффилиация

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