preimage_const_add_Icc

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

Under translation by a, the preimage of Icc [b, c] is [b − a, c − a].

Русский

При смещении на a предобраз Icc [b, c] равен [b − a, c − a].

LaTeX

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

Lean4

@[simp]
theorem preimage_const_add_Icc : (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a) := by simp [← Ici_inter_Iic]

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

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

Разделы

Аффилиация

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