preimage_sub_const_Ioi

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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