English
If k ≤ n, subtract k from every element of Ico n m yields Ico (n−k) (m−k).
Русский
Если k ≤ n, вычитая k из каждого элемента Ico n m, получаем Ico (n−k) (m−k).
LaTeX
$$$\forall n,m,k:\ k \le n \Rightarrow (\operatorname{Ico}(n,m)).\operatorname{map}(x \mapsto x-k) = \operatorname{Ico}(n-k,m-k).$$$
Lean4
theorem map_sub (n m k : ℕ) (h₁ : k ≤ n) : ((Ico n m).map fun x => x - k) = Ico (n - k) (m - k) := by
rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]