map_add_left_Ioo — Mathlib

English

Translating the open interval Ioo(a,b) by c on the left yields Ioo(a+c, b+c).

Русский

Сдвиг Ioo(a,b) на c слева дает Ioo(a+c, b+c).

LaTeX

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

Lean4

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

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