preimage_add_const_Ioc

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

The preimage of Ioc [b, c) under x ↦ a + x is Ioc[b − a, c − a).

Русский

Предобраз Ioc [b, c) под x ↦ a + x равен Ioc[b − a, c − a).

LaTeX

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

Lean4

@[simp]
theorem preimage_add_const_Ioc : (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a) := by simp [← Ioi_inter_Iic]

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

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

Разделы

Аффилиация

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