map_add_left_Ioc — Mathlib

English

Translating the half-open-to-closed interval Ioc(a,b) by c on the left yields Ioc(a+c, b+c).

Русский

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

LaTeX

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

Lean4

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

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