preimage_add_const_Ico

Mathlib.Algebra.Order.Group.Pointwise.Interval

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_add_const_Ico : (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a) := by simp [← Ici_inter_Iio]

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

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

Разделы

Аффилиация

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