map_add_left_Icc — Mathlib

English

Adding a constant c to every element of the closed interval Icc(a,b) shifts the interval by c: map (c + ·) of Icc(a,b) equals Icc(a+c, b+c).

Русский

Прибавление константы c к каждому элементу множества, получаемого из Icc(a,b), сдвигает интервал: отображение (+c) от Icc(a,b) равно Icc(a+c, b+c).

LaTeX

$$$\text{Multiset.map} (\lambda x, c+x)\, (\text{Multiset.Icc } a b) = \text{Multiset.Icc } (a+c) (b+c)$$$

Lean4

theorem map_add_left_Icc (a b c : α) : (Icc a b).map (c + ·) = Icc (c + a) (c + b) := by
  classical
    rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]

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